IMap
spec
IntSet
spec
Internal
proof
InvariantFunction
lang
Iterable
spec
Iterator
spec
i
UpdatedArray
iff
LogicalOps
ignore
annotation
implies
LogicalOps
in
Passes
indexOf
List
indexWhere
List
List
index_defined
MapArrayLemmas
induct
annotation
init
List
List
PList
inline
annotation
insert
DistinctList
DistinctListOps
SortedListOps
SortedListTakeOps
AHeap
AVLTreeOps
ArrayHeap
HeapADT
IntSet
LeftistHeapOps
ListHeap
ListSetOps
TreeSet
insertAll
DistinctList
insertAt
List
List
insert_bisim
ArrayHeapListHeapBisim
insert_comm
SortedListLemmas
insert_comm_lemma
SortedListTakeLemmas
insert_comm_prop
Heap_List_BisimulationSpec
LeftistHeapSpec
LeftistHeapSpec0
insert_commu_lemma
FIFOMapSpec
PairMapSpec
SetMapSpec
insert_commutative_prop
SortedListSpec
SortedListTakeSpec
insert_delete
SortedListLemmas
insert_invariant
LeftistHeapSpec
SetAggregationProof
insert_merge
SortedListTakeLemmas
insert_merge_perm
SortedListTakeLemmas
insert_sort_delete
SortedListLemmas
int32_add_lemma
PrimitiveDataTypeSpec
int32_vector_add_lemma
PrimitiveDataTypeSpec
int_vector_add_lemma
PrimitiveDataTypeSpec
integer_add_lemma
PrimitiveDataTypeSpec
integer_max_lemma
PrimitiveDataTypeSpec
internal
annotation
intersect
List
inv
ArrayHeap
ArrayList
ArrayQueue
ArrayStack
BoundedArray
MapArray
MapArrayList
invariant
InvariantFunction
isBlack
BlackTree
Leaf
RedTree
Tree
isDefined
Option
isDefinedAt
Map
List
isDefinedBetween
IMap
isEmpty
List
Option
Set
List
PList
ArrayHeap
HeapNode
ListADT
MapArray
isHeap
HeapADT
LeftistHeapOps
ListHeap
isLeft
Either
Left
Right
isPartiallyOrdered
LeftistHeap
isPrefixOf
List
isRational
Rational
isRed
BlackTree
Leaf
RedTree
Tree
isRight
Either
Left
Right
isSorted
ListOps
SortedListOps
isSuffixOf
List
is_descendant_of_zero
AHeap
is_min
MinLemmas
isabelle
annotation
iterator
ArrayList
CollectionImpl
Iterable
LinkedList
MapArrayList
iterator_bisim
LinkedListArrayListBisimulation
LinkedListMapArrayListBisimulation