Session HOL

Theories

• Code_Generator
• HOL
• Orderings
• Groups
• Lattices
• Set
• Typedef
• Fun
• Complete_Lattices
• Ctr_Sugar
• Inductive
• Product_Type
• Sum_Type
• Rings
• Nat
• Fields
• Finite_Set
• Relation
• Transitive_Closure
• Wellfounded
• Wfrec
• Order_Relation
• Hilbert_Choice
• Zorn
• BNF_Wellorder_Relation
• BNF_Wellorder_Embedding
• BNF_Wellorder_Constructions
• BNF_Cardinal_Order_Relation
• BNF_Cardinal_Arithmetic
• Fun_Def_Base
• BNF_Def
• BNF_Composition
• Basic_BNFs
• BNF_Fixpoint_Base
• BNF_Least_Fixpoint
• Basic_BNF_LFPs
• Meson
• ATP
• Metis
• Transfer
• Num
• Power
• Groups_Big
• Equiv_Relations
• Lifting
• Quotient
• Complete_Partial_Order
• Option
• Partial_Function
• Argo
• SAT
• Fun_Def
• Int
• Lattices_Big
• Euclidean_Division
• Parity
• Divides
• Numeral_Simprocs
• Semiring_Normalization
• Groebner_Basis
• Set_Interval
• Presburger
• SMT
• Sledgehammer
• Code_Numeral
• Lifting_Set
• List
• Groups_List
• Random
• Map
• Enum
• String
• Typerep
• Predicate
• Lazy_Sequence
• Limited_Sequence
• Code_Evaluation
• Quickcheck_Random
• Random_Pred
• Random_Sequence
• Quickcheck_Exhaustive
• Predicate_Compile
• Quickcheck_Narrowing
• Extraction
• Record
• GCD
• Nitpick
• Nunchaku
• BNF_Greatest_Fixpoint
• Filter
• Conditionally_Complete_Lattices
• Factorial
• Binomial
• Main
• Archimedean_Field
• Rat
• Real
• Topological_Spaces
• Hull
• Modules
• Vector_Spaces
• Real_Vector_Spaces
• Limits
• Inequalities
• Series
• Deriv
• NthRoot
• Transcendental
• Complex
• MacLaurin
• Complex_Main