Index of Isabelle/HOL/HOL-ex

Theories

• Adhoc_Overloading
• Monad_Syntax
• State_Monad
• Code_Binary_Nat
• Code_Natural
• Code_Integer
• Efficient_Nat
• Code_Binary_Nat_examples
• FuncSet
• Eval_Examples
• Normalization_by_Evaluation
• Hebrew
• Chinese
• Serbian
• Phantom_Type
• Cardinality
• FinFun
• FinFun_Syntax
• Refute
• Iff_Oracle
• Coercion_Examples
• Numeral_Representation
• Higher_Order_Logic
• Abstract_NAT
• Guess
• Binary
• Fundefs
• Induction_Schema
• LocaleTest2
• Records
• While_Combinator
• While_Combinator_Example
• MonoidGroup
• BinEx
• Hex_Bin_Examples
• Antiquote
• Multiquote
• PER
• NatSum
• LaTeXsugar
• ThreeDivides
• Intuitionistic
• CTL
• Arith_Examples
• BT
• Tree23
• AList
• DAList
• Multiset
• MergeSort
• Lagrange
• Groebner_Examples
• MT
• Unification
• Primrec
• Tarski
• Classical
• Set_Theory
• Meson_Test
• Termination
• Coherent
• PresburgerEx
• Reflection
• ReflectionEx
• Primes
• Sqrt
• Sqrt_Script
• Transfer_Ex
• Quotient_Syntax
• Quotient_Set
• Quotient_Product
• Quotient_Option
• Quotient_List
• Transfer_Int_Nat
• HarmonicSeries
• Refute_Examples
• Preorder
• Landau
• Mapping
• AList_Mapping
• Execute_Choice
• Summation
• Gauge_Integration
• Dedekind_Real
• Quicksort
• Birthday_Paradox
• List_to_Set_Comprehension_Examples
• Seq
• Simproc_Tests
• Executable_Relation
• FinFunPred
• Set_Comprehension_Pointfree_Tests
• Parallel
• Debug
• Parallel_Example
• IArray
• IArray_Examples
• SVC_Oracle