# HG changeset patch
# User wenzelm
# Date 1492803692 -7200
# Node ID 263f2a046308b94b69f04e422a5067f58e86205c
# Parent  b7caa2b8bdbfdc027e4cacc9604eac66fa78b206
tuned;

diff -r b7caa2b8bdbf -r 263f2a046308 src/HOL/ROOT
--- 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]