Session HOL-Data_Structures

Theories

• Less_False
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• Sorting
• HOL-Library.Tree
• HOL-Library.Tree_Real
• Balance
• Cmp
• Sorted_Less
• List_Ins_Del
• Set_Specs
• Tree_Set
• AList_Upd_Del
• Map_Specs
• Tree_Map
• Tree_Rotations
• Tree2
• Isin2
• Interval_Tree
• AVL_Set_Code
• HOL-Number_Theory.Fib
• AVL_Set
• Lookup2
• AVL_Map
• AVL_Bal_Set
• AVL_Bal2_Set
• Height_Balanced_Tree
• RBT
• RBT_Set
• RBT_Set2
• RBT_Map
• Tree23
• Tree23_Set
• Tree23_Map
• Define_Time_Function
  • File ‹Define_Time_0.ML›
  • File ‹Define_Time_Function.ML›
• Tree23_of_List
• Tree234
• Tree234_Set
• Tree234_Map
• Brother12_Set
• Brother12_Map
• AA_Set
• AA_Map
• Set2_Join
• Set2_Join_RBT
• Time_Funs
• Array_Specs
• Braun_Tree
• Array_Braun
• Trie_Fun
• Trie_Map
• Tries_Binary
• Queue_Spec
• Reverse
• Queue_2Lists
• HOL-Library.Tree_Multiset
• Priority_Queue_Specs
• Heaps
• HOL-Library.Pattern_Aliases
• Leftist_Heap
• Leftist_Heap_List
• Binomial_Heap
• Selection