tuned;

--- a/src/HOL/ex/Antiquote.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/Antiquote.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -2,14 +2,17 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Simple quote / antiquote example.
 *)
 
 header {* Antiquotations *}
 
 theory Antiquote = Main:
 
+text {*
+  A simple example on quote / antiquote in higher-order abstract
+  syntax.
+*}
+
 syntax
   "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
 
@@ -35,4 +38,3 @@
 term "Expr (\<lambda>env. f env + g env y + h a env z)"
 
 end
-

--- a/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -2,15 +2,17 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Multiple nested quotations and anti-quotations -- basically a
-generalized version of de-Bruijn representation.
 *)
 
 header {* Multiple nested quotations and anti-quotations *}
 
 theory Multiquote = Main:
 
+text {*
+  Multiple nested quotations and anti-quotations -- basically a
+  generalized version of de-Bruijn representation.
+*}
+
 syntax
   "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
   "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)

--- a/src/HOL/ex/NatSum.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/NatSum.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -36,7 +36,8 @@
 *}
 
 lemma sum_of_odd_squares:
-  "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = n * (#4 * n * n - #1)"
+  "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
+    n * (#4 * n * n - #1)"
   apply (induct n)
   txt {* This removes the @{term "-#1"} from the inductive step *}
    apply (case_tac [2] n)
@@ -61,17 +62,20 @@
   \medskip The sum of the first @{term n} positive integers equals
   @{text "n (n + 1) / 2"}.*}
 
-lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n"
+lemma sum_of_naturals:
+    "#2 * setsum id (atMost n) = n * Suc n"
   apply (induct n)
    apply auto
   done
 
-lemma sum_of_squares: "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
+lemma sum_of_squares:
+    "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
   apply (induct n)
    apply auto
   done
 
-lemma sum_of_cubes: "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
+lemma sum_of_cubes:
+    "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
   apply (induct n)
    apply auto
   done

--- a/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:08 2001 +0200
@@ -8,6 +8,20 @@
 time_use_thy "Recdefs";
 time_use_thy "Primrec";
 
+setmp proofs 2 time_use_thy "Hilbert_Classical";
+
+(*advanced concrete syntax*)
+time_use_thy "Tuple";
+time_use_thy "Antiquote";
+time_use_thy "Multiquote";
+
+(*basic use of extensible records*)
+time_use_thy "MonoidGroup";
+time_use_thy "Records";
+
+time_use_thy "StringEx";
+time_use_thy "BinEx";
+
 time_use_thy "NatSum";
 time_use     "cla.ML";
 time_use     "mesontest.ML";
@@ -24,16 +38,4 @@
 time_use_thy "MT";
 time_use_thy "Tarski";
 
-time_use_thy "StringEx";
-time_use_thy "BinEx";
-
 if_svc_enabled time_use_thy "svc_test";
-
-(*basic use of extensible records*)
-time_use_thy "MonoidGroup";
-time_use_thy "Records";
-
-(*advanced concrete syntax*)
-time_use_thy "Tuple";
-time_use_thy "Antiquote";
-time_use_thy "Multiquote";

--- a/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -15,7 +15,8 @@
 lemma "''ABCD'' = ''ABCD''"
   by simp
 
-lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq> ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
+lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
+  ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
   by simp
 
 lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"

--- a/src/HOL/ex/mesontest2.thy	Thu Sep 27 15:42:01 2001 +0200
+++ b/src/HOL/ex/mesontest2.thy	Thu Sep 27 15:42:08 2001 +0200
@@ -1,8 +1,7 @@
 
-(*Theory Product_Type instead of HOL regards arguments as tuples.
-  But theory Main would allow clashes with many other constants.*)
+header {* Meson test cases *}
 
-theory mesontest2 = Product_Type:
+theory mesontest2 = Main:
 
 hide const inverse divide