Task
par
Tree
RedBlackTree
TreeNode
AVLTree
TreeSet
spec
t
Cons
Cons
PCons
tail
List
List
PList
ArrayList
LinkedList
ListADT
MapArrayList
tailOption
List
tail_bisim
LinkedListArrayListBisimulation
LinkedListMapArrayListBisimulation
take
List
List
PList
ListArray
MapArray
takeRight
List
takeWhile
List
List
PList
take_all
ListLemmas
SortedListTakeLemmas
take_delete
SortedListTakeLemmas
take_forall
MapArrayLemmas
take_idempotent
SortedListTakeLemmas
take_n_m
SortedListTakeLemmas
take_toList
MapArrayLemmas
task
par
theMap
Map
theSet
Set
toHeap
Heap_List_BisimulationSpec
LeftistHeapSpec0
toLeftistHeap
HeapNode
toList
Option
SetOps
AVLTreeOps
ArrayHeap
Heap_List_BisimulationSpec
IMap
Iterator
HeapNode
LeftistHeapOps
ListArray
ListHeap
ListIterator
MapArray
toList_append
IMap
toList_cons
IMap
toList_contains
IMap
toList_copy
IMap
toList_drop
IMap
toList_snoc
IMap
toList_take
IMap
toMap
ListOps
toSet
List
Option
AVLTreeOps
toSortedList
AVLTreeOps
HeapADT
LeftistHeapOps
ListHeap
to_imap
MapArrayLemmas
to_list_size_eq
ArrayListLemmas
top
ArrayStack
ListStack
transitive
AHeap
tree
AVLTreeOps
TreeSet
trivial
proof
typ
isabelle