Session HOL-ex

Theories

• Antiquote
• Argo_Examples
• Arith_Examples
• Ballot
• BigO
• BinEx
• Birthday_Paradox
• Bubblesort
• CTL
• Cartouche_Examples
• Case_Product
• Chinese
• Classical
• Code_Binary_Nat_examples
• Code_Lazy_Demo
• Code_Timing
• Coercion_Examples
• Computations
• Conditional_Parametricity_Examples
• Cubic_Quartic
• Datatype_Record_Examples
• Erdoes_Szekeres
• Eval_Examples
• Executable_Relation
• Execute_Choice
• Function_Growth
• Gauge_Integration
• HarmonicSeries
• Hebrew
• Hex_Bin_Examples
• IArray_Examples
• Intuitionistic
• Join_Theory
• Lagrange
• List_to_Set_Comprehension_Examples
• LocaleTest2
• MergeSort
• MonoidGroup
• Multiquote
• NatSum
• Normalization_by_Evaluation
• PER
• Parallel_Example
• Peano_Axioms
• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Perm
• Perm_Fragments
• PresburgerEx
• Pythagoras
• Quicksort
• Radix_Sort
• Reflection_Examples
• Refute_Examples
• Residue_Ring
• SOS
• SOS_Cert
• Serbian
• Set_Comprehension_Pointfree_Examples
• Set_Theory
• Simproc_Tests
• Simps_Case_Conv_Examples
• Sketch_and_Explore
• Sorting_Algorithms_Examples
• Specifications_with_bundle_mixins
• Sqrt_Script
• Sudoku
• Tarski
• Termination
• ThreeDivides
• Transfer_Debug
• Transfer_Int_Nat
• Transitive_Closure_Table_Ex
• Tree23
• Triangular_Numbers
• Unification
• While_Combinator_Example
• veriT_Preprocessing
• SAT_Examples
• Meson_Test