Session Collections

Theories

• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• Binomial-Heaps.BinomialHeap
• Binomial-Heaps.SkewBinomialHeap
• Finger-Trees.FingerTree
• Sorted_List_Operations
• Word_Lib.More_Arithmetic
• Word_Lib.More_Divides
• Word_Lib.More_Bit_Ring
• Word_Lib.More_Word
• Word_Lib.Bit_Shifts_Infix_Syntax
• Word_Lib.Most_significant_bit
• Word_Lib.Least_significant_bit
• Word_Lib.Generic_set_bit
• Word_Lib.Bit_Comprehension
• HOL-Library.Signed_Division
• Word_Lib.Signed_Division_Word
• Native_Word.Code_Target_Word_Base
• Native_Word.Word_Type_Copies
• Native_Word.Code_Int_Integer_Conversion
• Native_Word.Code_Target_Integer_Bit
• Native_Word.Uint32
• HashCode
• Native_Word.Code_Target_Int_Bit
• Code_Target_ICF
• HOL-Library.RBT_Impl
• SetIterator
• SetIteratorOperations
• Proper_Iterator
• It_to_It
• SetIteratorGA
• Gen_Iterator
• Idx_Iterator
• Iterator
• RBT_add
• HOL-Library.Confluence
• HOL-Library.Confluent_Quotient
• HOL-Library.Dlist
• Dlist_add
• HOL-Library.AList
• Assoc_List
• Diff_Array
• Partial_Equivalence_Relation
• ICF_Tools
• Ord_Code_Preproc
• Record_Intf
• Locale_Code
• ICF_Spec_Base
• MapSpec
• Robdd
• Locale_Code_Ex
• DatRef
• SetAbstractionIterator
• GenCF_Chapter
• GenCF_Intf_Chapter
• Intf_Map
• Intf_Set
• Intf_Hash
• Intf_Comp
• GenCF_Gen_Chapter
• Gen_Set
• Gen_Map
• Gen_Map2Set
• HOL-Library.Product_Lexorder
• Gen_Comp
• GenCF_Impl_Chapter
• Impl_Array_Stack
• Impl_List_Set
• Array_Iterator
• Impl_List_Map
• Impl_Array_Hash_Map
• Impl_RBT_Map
• Impl_Cfun_Set
• Impl_Array_Map
• Impl_Bit_Set
• Native_Word.Uint
• Impl_Uv_Set
• Gen_Hash
• GenCF
• ICF_Chapter
• ICF_Spec_Chapter
• SetSpec
• ListSpec
• AnnotatedListSpec
• PrioSpec
• PrioUniqueSpec
• ICF_Gen_Algo_Chapter
• SetIteratorCollectionsGA
• MapGA
• SetGA
• SetByMap
• ListGA
• SetIndex
• Algos
• PrioByAnnotatedList
• PrioUniqueByAnnotatedList
• ICF_Impl_Chapter
• ListMapImpl
• ListMapImpl_Invar
• HOL-Library.RBT
• RBTMapImpl
• HashMap_Impl
• HashMap
• Trie.Trie
• Trie_Impl
• Trie2
• TrieMapImpl
• ArrayHashMap_Impl
• ArrayHashMap
• ArrayMapImpl
• MapStdImpl
• ListSetImpl
• ListSetImpl_Invar
• ListSetImpl_NotDist
• ListSetImpl_Sorted
• RBTSetImpl
• HashSet
• TrieSetImpl
• ArrayHashSet
• ArraySetImpl
• SetStdImpl
• Fifo
• BinoPrioImpl
• SkewPrioImpl
• FTAnnotatedListImpl
• FTPrioImpl
• FTPrioUniqueImpl
• ICF_Impl
• ICF_Refine_Monadic
• ICF_Autoref
• ICF_Entrypoints_Chapter
• Collections
• CollectionsV1
• Collections_Entrypoints_Chapter
• Refine_Dflt
• Refine_Dflt_ICF
• Refine_Dflt_Only_ICF
• Userguides_Chapter
• Refine_Monadic_Userguide
• ICF_Userguide