PCons
PairList
PList
PairList
PNil
PairList
Pair
PairList
PairList
collection
PairListLemmas
proof
PairMapLemmas
spec
PairMapSpec
spec
Passes
lang
PermutationLemmas
proof
PermutationOps
proof
PrimitiveDataTypeSpec
spec
ProofOps
proof
padTo
List
List
par
leon
parallel
par
parent
AHeap
partially_ordered
AHeap
partially_ordered_at
AHeap
partially_ordered_is_well_ordered
AHeap
partially_ordered_swap
AHeap
partition
List
List
PList
passes
Passes
percolatingDown
AHeap
percolatingDown_compare
AHeap
percolatingDown_else
AHeap
percolatingDown_ind
AHeap
percolatingDown_op
AHeap
percolatingDown_perm
AHeap
percolatingDown_root
AHeap
percolatingDown_sibling
AHeap
percolatingDown_valid
AHeap
percolatingDown_value_unchanged
AHeap
percolatingUp
AHeap
percolatingUp_ind
AHeap
percolatingUp_ind1
AHeap
percolatingUp_ind2
AHeap
percolatingUp_ind3
AHeap
percolatingUp_op
AHeap
percolatingUp_perm
AHeap
percolatingUp_root
AHeap
percolatingUp_valid
AHeap
perm_delete_contains
DistinctLemmas
ListSetLemmas
permutation
PairList
PermutationOps
permutation3
PermutationLemmas
permutation3_swap2
PermutationLemmas
permutation3_swap_noassoc
PermutationLemmas
permutation_append
PairListLemmas
PermutationLemmas
permutation_by_tran
PairListLemmas
permutation_car_swap
PairListLemmas
PermutationLemmas
permutation_comm
PairListLemmas
PermutationLemmas
permutation_comm_lemma
PairListLemmas
permutation_concat
PermutationLemmas
permutation_concat_assoc
PairListLemmas
PermutationLemmas
permutation_concat_comm
PairListLemmas
PermutationLemmas
permutation_concat_move
PermutationLemmas
permutation_cons
PairListLemmas
PermutationLemmas
permutation_cons_delete
PermutationLemmas
permutation_cons_tail
PairListLemmas
PermutationLemmas
permutation_contains
DistinctLemmas
ListSetLemmas
permutation_contains_lemma
PairListLemmas
permutation_content
PairListLemmas
PermutationLemmas
permutation_content_lemma
PairListLemmas
permutation_delete
PairListLemmas
PermutationLemmas
permutation_delete_cons
PairListLemmas
PermutationLemmas
permutation_delete_head
PairListLemmas
permutation_eq
PairListLemmas
PermutationLemmas
permutation_filter_contains
PairListLemmas
permutation_first_last_swap
SortedListTakeLemmas
permutation_getAll_lemma
PairListLemmas
permutation_hasKey_lemma
PairListLemmas
permutation_not_contains
DistinctLemmas
ListSetLemmas
permutation_prefix
PairListLemmas
permutation_prepend
PermutationLemmas
permutation_refl
PairListLemmas
PermutationLemmas
permutation_replace
PermutationLemmas
permutation_sort
SortedListLemmas
permutation_sort_prop
SortedListSpec
permutation_tail_delete
PermutationLemmas
permutation_tran
PairListLemmas
PermutationLemmas
permutation_tran_lemma
PairListLemmas
permutation_tran_lemma2
PairListLemmas
PermutationLemmas
pop
ArrayStack
ListStack
prefixLength
List
prefix_tran
ListLemmas
prepend
ArrayList
LinkedList
ListADT
MapArray
MapArrayList
prepend_bisim
LinkedListArrayListBisimulation
LinkedListMapArrayListBisimulation
prepend_head
ArrayListLemmas
prepend_toList
MapArrayLemmas
proof
isabelle
leon
WithProof
libref
prop
WithProof
WithRel
ProofOps
RelReasoning
push
ArrayStack
ListStack
put
State