Session Van_Emde_Boas_Trees

Theories

• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Imperative_HOL.Heap
• HOL-Library.Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• HOL-Library.Monad_Syntax
• Heap_Time_Monad
• Array_Time
• Ref_Time
• Imperative_HOL_Time
• Syntax_Match
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• HOL-ex.Quicksort
• HOL-Library.Option_ord
• HOL-Library.Infinite_Set
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Automatic_Refinement.Misc
• Assertions
• Hoare_Triple
• Refine_Imp_Hol
• Automation
• Sep_Main
• HOL-Imperative_HOL.Heap_Monad
• HOL-Imperative_HOL.Array
• HOL-Imperative_HOL.Ref
• HOL-Imperative_HOL.Imperative_HOL
• Imperative_HOL_Add
• Time_Reasoning
• Simple_TBOUND_Cond
• VEBT_Example_Setup
• HOL-Library.Countable_Set
• HOL-Library.Countable_Complete_Lattices
• HOL-Library.Order_Continuity
• HOL-Library.Extended_Nat
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• VEBT_Definitions
• VEBT_Member
• VEBT_Insert
• VEBT_InsertCorrectness
• VEBT_MinMax
• VEBT_Succ
• VEBT_Pred
• VEBT_Delete
• VEBT_DeleteCorrectness
• VEBT_Uniqueness
• VEBT_Height
• VEBT_Bounds
• VEBT_DeleteBounds
• VEBT_Space
• VEBT_Intf_Functional
• HOL-Library.Rewrite
  • File ‹cconv.ML›
  • File ‹rewrite.ML›
• VEBT_List_Assn
• Deriving.Generator_Aux
  • File ‹bnf_access.ML›
  • File ‹generator_aux.ML›
• Deriving.Derive_Manager
  • File ‹derive_manager.ML›
• Deriving.Comparator
• Deriving.Comparator_Generator
  • File ‹comparator_generator.ML›
• Deriving.Compare
  • File ‹compare_code.ML›
• Deriving.Compare_Generator
  • File ‹compare_generator.ML›
• HOL-Library.Char_ord
• Deriving.Compare_Instances
• Deriving.Equality_Generator
  • File ‹equality_generator.ML›
• Deriving.Equality_Instances
• HOL-Library.Phantom_Type
• HOL-Library.Cardinality
• HOL-Library.Numeral_Type
• HOL-Library.Type_Length
• HOL-Library.Word
  • File ‹Tools/word_lib.ML›
  • File ‹Tools/smt_word.ML›
• 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
• Collections.HashCode
• Deriving.Hash_Generator
  • File ‹hash_generator.ML›
• Deriving.Hash_Instances
• Deriving.Countable_Generator
• Deriving.Derive
• VEBT_BuildupMemImp
• VEBT_SuccPredImperative
• VEBT_DelImperative
• VEBT_Intf_Imperative
• VEBT_Example