FIFOMapLemmas
spec
FIFOMapSpec
spec
FunctionalArray
spec
FunctionalArrayLemmas
spec
fill
List
List
filter
List
Option
List
PList
SetOps
filterM
State
filterNot
List
List
PList
filter_complete
PairListLemmas
filter_disjoint
PairListLemmas
filter_sound
PairListLemmas
filter_union_content
PairListLemmas
filter_union_perm
PairListLemmas
filter_union_perm1
PairListLemmas
filter_union_perm2
PairListLemmas
filter_union_size
PairListLemmas
find
List
List
PList
RedBlackTree
findMax
AVLTreeOps
IntSet
RedBlackTree
TreeSet
findMin
AVLTreeOps
ArrayHeap
HeapADT
IntSet
LeftistHeapOps
ListHeap
RedBlackTree
TreeSet
findMin_bisim
ArrayHeapListHeapBisim
findMin_invariant
LeftistHeapSpec
findMin_toList_min
BigIntArrayHeap
findNth
RedBlackTree
first
ArrayQueue
ListQueue
flatMap
List
Option
State
List
flatten
ListOps
ListOps
flattenPreservesContent
ListSpecs
ListLemmas
foldLeft
List
List
PList
foldLeftM
State
foldLeftM_
State
foldRight
List
List
PList
foldl_insert
SortedListTakeOps
LeftistHeap
foldl_insert_2
SortedListTakeLemmas
foldl_insert_3
SortedListTakeLemmas
foldl_insert_lemma
SortedListTakeLemmas
folds
ListSpecs
ListLemmas
forall
List
lang
Option
List
PList
SetOps
IMap
ListArray
MapArray
forallAssoc
ListLemmas
forall_exists
ListLemmas
forall_p_not_in
PairListLemmas
forall_shrink
IMap
forall_tran
IMap
from
MapArray
fullBody
isabelle
function
isabelle