Session HOL-ex

Theories

• Adhoc_Overloading
• Monad_Syntax
• State_Monad
• Code_Abstract_Nat
• Code_Binary_Nat
• Code_Binary_Nat_examples
• FuncSet
• Eval_Examples
• Normalization_by_Evaluation
• Hebrew
• Chinese
• Serbian
• Phantom_Type
• Cardinality
• FinFun
• FinFun_Syntax
• Refute
• Transitive_Closure_Table
• Cartouche_Examples
• Infinite_Set
• Adhoc_Overloading_Examples
• Iff_Oracle
• Coercion_Examples
• Higher_Order_Logic
• Abstract_NAT
• Guess
• 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
• Multiset
• MergeSort
• Lagrange
• Groebner_Examples
• MT
• Unification
• Primrec
• Tarski
• Classical
• Set_Theory
• Termination
• Coherent
• PresburgerEx
• Reflection
• Reflection_Examples
• Primes
• Sqrt
• Sqrt_Script
• Transfer_Int_Nat
• Transfer_Ex
• Transitive_Closure_Table_Ex
• HarmonicSeries
• Refute_Examples
• AList
• Mapping
• AList_Mapping
• Execute_Choice
• Gauge_Integration
• Dedekind_Real
• Quicksort
• Birthday_Paradox
• List_to_Set_Comprehension_Examples
• Seq
• Simproc_Tests
• Executable_Relation
• FinFunPred
• Set_Comprehension_Pointfree_Examples
• Parallel
• Debug
• Parallel_Example
• IArray
• Code_Target_Int
• Code_Target_Nat
• Code_Target_Numeral
• IArray_Examples
• SVC_Oracle
• Simps_Case_Conv
• Simps_Case_Conv_Examples
• ML
• SAT_Examples
• Sudoku
• Nominal2_Dummy
• Meson_Test