Index of Isabelle/HOL-Proofs

Theories

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