Session HOL-Proofs

Theories

• Proofs
• Code_Generator
• HOL
• Orderings
• Groups
• Lattices
• Set
• Typedef
• Fun
• Complete_Lattices
• Ctr_Sugar
• Inductive
• Product_Type
• Sum_Type
• Rings
• Fields
• Nat
• Finite_Set
• Groups_Big
• Relation
• Equiv_Relations
• Datatype
• Transitive_Closure
• Wellfounded
• Wfrec
• Order_Relation
• Hilbert_Choice
• Zorn
• BNF_Wellorder_Relation
• BNF_Wellorder_Embedding
• BNF_Constructions_on_Wellorders
• BNF_Cardinal_Order_Relation
• BNF_Cardinal_Arithmetic
• Fun_Def_Base
• BNF_Def
• BNF_Comp
• Basic_BNFs
• BNF_FP_Base
• BNF_LFP
• Num
• Power
• Meson
• ATP
• Metis
• Option
• Transfer
• Lifting
• Quotient
• Complete_Partial_Order
• Partial_Function
• SAT
• Fun_Def
• Int
• Nat_Transfer
• Divides
• Numeral_Simprocs
• Semiring_Normalization
• Groebner_Basis
• Lattices_Big
• Set_Interval
• Presburger
• SMT2
• Sledgehammer
• Code_Numeral
• Lifting_Set
• Lifting_Option
• Lifting_Product
• 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
• Lifting_Sum
• Coinduction
• Record
• Nitpick
• BNF_GFP
• SMT
• Main