Collection
spec
CollectionImpl
spec
Cons
collection
collection
c
Task
ArrayHeap
check
proof
child_is_descendant
AHeap
choose
synthesis
chunks
List
List
collection
leon
libref
comb
SetAggregationProof
comb_assoc_lemma
SetAggregationProof
comb_comm_lemma
SetAggregationProof
compare
BigIntArrayHeap
compose
annotation
composition_prop
SortedListTakeSpec
LeftistHeapSpec
LeftistHeapSpec0
computes
SpecsDecorations
concat
StrOps
concat_contains
ListLemmas
concat_permutation
PairListLemmas
PermutationLemmas
concat_permutation_lemma
PairListLemmas
consIndex
ListSpecs
consIsAppend
ListLemmas
cons_concat_perm1
PermutationLemmas
cons_concat_perm2
PermutationLemmas
cons_delete_perm
PairListLemmas
cons_distinct_assoc
DistinctLemmas
ListSetLemmas
cons_merge_assoc
PairListLemmas
cons_snoc_perm
PermutationLemmas
constructor
isabelle
contains
List
Map
Set
List
PList
AVLTreeOps
IntSet
RedBlackTree
TreeSet
contains_count
ListLemmas
content
List
Left
Right
List
PList
HeapADT
ListHeap
copy
IMap
copy_defined_at
IMap
copy_defined_between
IMap
copy_forall
IMap
corr
SetAggregationProof
count
List
List
PList
BlackTree
Leaf
RedTree
Tree
countAssoc
ListLemmas
count_contains
ListLemmas
create
MapArray
cut_as_take_drop
ListLemmas