Index of Isabelle/HOL-Proofs

Theories

• Code_Generator
• HOL
• Orderings
• Groups
• Lattices
• Set
• Typedef
• Complete_Lattices
• Inductive
• Fun
• Product_Type
• Sum_Type
• Rings
• Fields
• Nat
• Datatype
• Complete_Partial_Order
• Option
• Partial_Function
• SAT
• Num
• Power
• Finite_Set
• Relation
• Transitive_Closure
• Wellfounded
• FunDef
• Extraction
• Meson
• ATP
• Metis
• Plain
• Big_Operators
• Equiv_Relations
• Hilbert_Choice
• Transfer
• Lifting
• Quotient
• Int
• Nat_Transfer
• Divides
• Code_Numeral
• Numeral_Simprocs
• Semiring_Normalization
• Groebner_Basis
• Set_Interval
• Presburger
• List
• Random
• Map
• Enum
• String
• Typerep
• Predicate
• Lazy_Sequence
• DSequence
• New_DSequence
• Code_Evaluation
• Quickcheck
• Random_Sequence
• New_Random_Sequence
• Quickcheck_Exhaustive
• Predicate_Compile
• Quickcheck_Narrowing
• Record
• SMT
• Sledgehammer
• Nitpick
• Main