Session HOL-Library

Theories

• README
• AList
• Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• BNF_Axiomatization
  • File ‹~~/src/HOL/Tools/BNF/bnf_axiomatization.ML›
• BNF_Corec
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
• While_Combinator
• Bourbaki_Witt_Fixpoint
• Centered_Division
• Char_ord
• Phantom_Type
• Cardinality
• Code_Cardinality
• Case_Converter
  • File ‹case_converter.ML›
• Code_Lazy
  • File ‹code_lazy.ML›
• Code_Test
  • File ‹code_test.ML›
• Combine_PER
• Complete_Partial_Order2
• Conditional_Parametricity
  • File ‹conditional_parametricity.ML›
• Confluence
• Confluent_Quotient
• Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• Nat_Bijection
• Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• Infinite_Set
• Countable_Set
• Countable_Complete_Lattices
• Countable_Set_Type
• Debug
• Diagonal_Subsequence
• Discrete
• FuncSet
• Disjoint_Sets
• FSet
• Finite_Map
• Disjoint_FSets
• Dlist
• Dual_Ordered_Lattice
• Equipollence
• Simps_Case_Conv
  • File ‹simps_case_conv.ML›
• Extended
• Order_Continuity
• Extended_Nat
• Liminf_Limsup
• Extended_Real
• Indicator_Function
• Extended_Nonnegative_Real
• Log_Nat
• Lattice_Algebras
• Float
• Function_Algebras
• Function_Division
• Fun_Lexorder
• Going_To_Filter
• Groups_Big_Fun
• Infinite_Typeclass
• Set_Algebras
• Interval
• Interval_Float
• IArray
• Landau_Symbols
• Lattice_Constructions
• Stream
• Sublist
• Linear_Temporal_Logic_on_Streams
• ListVector
• Lub_Glb
• Mapping
• Monad_Syntax
• More_List
• Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• Multiset
  • File ‹multiset_simprocs.ML›
• Multiset_Order
• NList
• Nonpos_Ints
• Numeral_Type
• Omega_Words_Fun
• Open_State_Syntax
• Option_ord
• Parallel
• Pattern_Aliases
• Periodic_Fun
• Poly_Mapping
• Power_By_Squaring
• Preorder
  • File ‹~~/src/Provers/preorder.ML›
• Product_Plus
• Quadratic_Discriminant
• Quotient_Syntax
• Quotient_Set
• Quotient_Product
• Quotient_Option
• Quotient_List
• Quotient_Sum
• Quotient_Type
• Ramsey
• Real_Mod
• Reflection
  • File ‹~~/src/HOL/Tools/reflection.ML›
• Rewrite
  • File ‹cconv.ML›
  • File ‹rewrite.ML›
• Type_Length
• Saturated
• Set_Idioms
• Signed_Division
• State_Monad
• Comparator
• Sorting_Algorithms
• Sum_of_Squares
  • File ‹Sum_of_Squares/positivstellensatz.ML›
  • File ‹Sum_of_Squares/positivstellensatz_tools.ML›
  • File ‹Sum_of_Squares/sum_of_squares.ML›
  • File ‹Sum_of_Squares/sos_wrapper.ML›
• Transitive_Closure_Table
• Tree
• Tree_Multiset
• Tree_Real
• Uprod
• Word
  • File ‹Tools/word_lib.ML›
  • File ‹Tools/smt_word.ML›
• Z2
• Library
• Product_Order
• Finite_Lattice
• List_Lexorder
• List_Lenlexorder
• Prefix_Order
• Product_Lexorder
• Subseq_Order
• Datatype_Records
  • File ‹datatype_records.ML›
• AList_Mapping
• Code_Abstract_Char
• Code_Abstract_Nat
• Code_Binary_Nat
• Code_Prolog
  • File ‹~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML›
• Code_Target_Int
• Code_Real_Approx_By_Float
• Code_Target_Nat
• Code_Target_Numeral
• Code_Target_Numeral_Float
• Complex_Order
• DAList
• DAList_Multiset
• RBT_Impl
• RBT
• RBT_Mapping
• RBT_Set
• LaTeXsugar
• OptionalSugar
• Predicate_Compile_Alternative_Defs
• Predicate_Compile_Quickcheck
  • File ‹~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML›
• Old_Recdef
  • File ‹old_recdef.ML›
• Realizers
  • File ‹~~/src/HOL/Tools/datatype_realizer.ML›
  • File ‹~~/src/HOL/Tools/inductive_realizer.ML›
• Refute
  • File ‹refute.ML›