--- a/src/HOL/ROOT Fri Apr 21 21:36:49 2017 +0200
+++ b/src/HOL/ROOT Fri Apr 21 21:41:32 2017 +0200
@@ -582,85 +582,85 @@
"HOL-Library"
"HOL-Number_Theory"
theories
- Code_Binary_Nat_examples
- Eval_Examples
- Normalization_by_Evaluation
- Hebrew
- Chinese
- Serbian
- Cartouche_Examples
- Computations
- Commands
Adhoc_Overloading_Examples
- Iff_Oracle
- Coercion_Examples
- Peano_Axioms
- Guess
- Functions
- Induction_Schema
- LocaleTest2
- Records
- While_Combinator_Example
- MonoidGroup
- BinEx
- Hex_Bin_Examples
Antiquote
- Multiquote
- PER
- NatSum
- ThreeDivides
+ Argo_Examples
+ Arith_Examples
+ Ballot
+ BinEx
+ Birthday_Paradox
+ Bubblesort
+ CTL
+ Cartouche_Examples
+ Chinese
+ Classical
+ Code_Binary_Nat_examples
+ Code_Timing
+ Coercion_Examples
+ Coherent
+ Commands
+ Computations
Cubic_Quartic
- Pythagoras
+ Dedekind_Real
+ Erdoes_Szekeres
+ Eval_Examples
+ Executable_Relation
+ Execute_Choice
+ Functions
+ Gauge_Integration
+ Groebner_Examples
+ Guess
+ HarmonicSeries
+ Hebrew
+ Hex_Bin_Examples
+ IArray_Examples
+ Iff_Oracle
+ Induction_Schema
Intuitionistic
- CTL
- Arith_Examples
- Tree23
- Bubblesort
+ Lagrange
+ List_to_Set_Comprehension_Examples
+ LocaleTest2
+ ML
MergeSort
- Lagrange
- Groebner_Examples
- Unification
+ MonoidGroup
+ Multiquote
+ NatSum
+ Normalization_by_Evaluation
+ PER
+ Parallel_Example
+ Peano_Axioms
+ Perm_Fragments
+ PresburgerEx
Primrec
- Tarski
- Classical
+ Pythagoras
+ Quicksort
+ Records
+ Reflection_Examples
+ Refute_Examples
+ Rewrite_Examples
+ SAT_Examples
+ SOS
+ SOS_Cert
+ Seq
+ Serbian
+ Set_Comprehension_Pointfree_Examples
Set_Theory
- Termination
- Coherent
- PresburgerEx
- Reflection_Examples
+ Simproc_Tests
+ Simps_Case_Conv_Examples
Sqrt
Sqrt_Script
+ Sudoku
+ Sum_of_Powers
+ Tarski
+ Termination
+ ThreeDivides
Transfer_Debug
Transfer_Ex
Transfer_Int_Nat
Transitive_Closure_Table_Ex
- HarmonicSeries
- Refute_Examples
- Execute_Choice
- Gauge_Integration
- Dedekind_Real
- Quicksort
- Birthday_Paradox
- List_to_Set_Comprehension_Examples
- Seq
- Simproc_Tests
- Executable_Relation
- Set_Comprehension_Pointfree_Examples
- Parallel_Example
- IArray_Examples
- Simps_Case_Conv_Examples
- ML
- Rewrite_Examples
- SAT_Examples
- SOS
- SOS_Cert
- Ballot
- Erdoes_Szekeres
- Sum_of_Powers
- Sudoku
- Code_Timing
- Perm_Fragments
- Argo_Examples
+ Tree23
+ Unification
+ While_Combinator_Example
Word_Type
veriT_Preprocessing
theories [skip_proofs = false]