# HG changeset patch
# User wenzelm
# Date 927891059 -7200
# Node ID cf6ad8d227930a86a407714f1362931cc1e78ccb
# Parent  74e8f703f5f2318585148012632f0516862c185a
tuned formal comments;

diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri May 28 13:30:59 1999 +0200
@@ -77,7 +77,7 @@
 qed;
 
 
-(* propositional proof (from 'Introduction to Isabelle') *)
+text {* propositional proof (from 'Introduction to Isabelle') *};
 
 lemma "P | P --> P";
 proof;
@@ -97,7 +97,7 @@
 qed;
 
 
-(* quantifier proof (from 'Introduction to Isabelle') *)
+text {* quantifier proof (from 'Introduction to Isabelle') *};
 
 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
 proof;
diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Fri May 28 13:30:59 1999 +0200
@@ -9,7 +9,7 @@
 theory Cantor = Main:;
 
 
-section "Example: Cantor's Theorem";
+section {* Example: Cantor's Theorem *};
 
 text {*
   Cantor's Theorem states that every set has more subsets than it has
diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Fri May 28 13:30:59 1999 +0200
@@ -7,12 +7,10 @@
 
 theory ExprCompiler = Main:;
 
-title
-  "Correctness of a simple expression/stack-machine compiler --- an Isabelle/Isar demonstration"
-  "Markus Wenzel";
+title {* Correctness of a simple expression/stack-machine compiler *};
 
 
-section "Basics";
+section {* Basics *};
 
 text {*
   First we define a type abbreviation for binary operations over some
@@ -23,7 +21,7 @@
   'val binop = "'val => 'val => 'val";
 
 
-section "Machine";
+section {* Machine *};
 
 text {*
   Next we model a simple stack machine, with three instructions.
@@ -55,7 +53,7 @@
   "execute instrs env == hd (exec instrs [] env)";
 
 
-section "Expressions";
+section {* Expressions *};
 
 text {*
   We introduce a simple language of expressions: variables ---
@@ -80,7 +78,7 @@
   "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
 
 
-section "Compiler";
+section {* Compiler *};
 
 text {*
   So we are ready to define the compilation function of expressions to
@@ -101,7 +99,6 @@
   @{term "comp"}.  We first establish some lemmas.
 *};
 
-
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
 proof (induct ??P xs type: list);
@@ -119,7 +116,6 @@
   qed;
 qed;
 
-
 lemma exec_comp:
   "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
 proof (induct ??P e type: expr);
@@ -133,7 +129,7 @@
 qed;
 
 
-text "Main theorem ahead.";
+text {* Main theorem ahead. *};
 
 theorem correctness: "execute (comp e) env = eval e env";
   by (simp add: execute_def exec_comp);
diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/NatSum.thy
--- a/src/HOL/Isar_examples/NatSum.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Fri May 28 13:30:59 1999 +0200
@@ -5,9 +5,9 @@
 
 theory NatSum = Main:;
 
-section "Summing natural numbers";
+section {* Summing natural numbers *};
 
-text "A summation operator: sum f (n+1) is the sum of all f(i), i=0...n.";
+text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
 
 consts
   sum	:: "[nat => nat, nat] => nat";
@@ -20,9 +20,9 @@
 (*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*)
 
 
-subsection "The sum of the first n positive integers equals n(n+1)/2";
+subsection {* The sum of the first n positive integers equals n(n+1)/2 *};
 
-text "Emulate Isabelle proof script:";
+text {* Emulate Isabelle proof script: *};
 
 (*
   Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
@@ -42,8 +42,8 @@
 qed_with sum_of_naturals;
 
 
-text "Proper Isabelle/Isar proof expressing the same reasoning (which
-  is apparently not the most natural one):";
+text {* Proper Isabelle/Isar proof expressing the same reasoning (which
+  is apparently not the most natural one): *};
 
 theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
 proof simp;
@@ -55,9 +55,9 @@
 qed;
 
 
-subsection "The sum of the first n odd numbers equals n squared";
+subsection {* The sum of the first n odd numbers equals n squared *};
 
-text "First version: `proof-by-induction'";
+text {* First version: `proof-by-induction' *};
 
 theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
 proof (induct n);
@@ -65,8 +65,8 @@
   fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
 qed;
 
-text "The second version tells more about what is going on during the
-induction.";
+text {* The second version tells more about what is going on during the
+induction. *};
 
 theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
 proof (induct n);
diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Fri May 28 13:30:59 1999 +0200
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Isar_examples/Peirce.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
-
-Peirce's law: examples of classical proof.
 *)
 
 theory Peirce = Main:;
 
+text {* Peirce's law: examples of classical proof. *};
 
 theorem "((A --> B) --> A) --> A";
 proof;
diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/ex/Points.thy
--- a/src/HOL/ex/Points.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/ex/Points.thy	Fri May 28 13:30:59 1999 +0200
@@ -5,11 +5,11 @@
 
 theory Points = Main:;
 
-title "Basic use of extensible records in HOL, including the famous points
- and coloured points.";
+title {* Basic use of extensible records in HOL, including the famous points
+ and coloured points. *};
 
 
-section "Points";
+section {* Points *};
 
 record point =
   x :: nat
@@ -42,14 +42,14 @@
 consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)";
 
 
-subsection "Introducing concrete records and record schemes";
+subsection {* Introducing concrete records and record schemes *};
 
 defs
   foo1_def: "foo1 == (| x = 1, y = 0 |)"
   foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
 
 
-subsection "Record selection and record update";
+subsection {* Record selection and record update *};
 
 constdefs
   getX :: "('a::more) point_scheme => nat"
@@ -58,13 +58,13 @@
   "setX r n == r (| x := n |)";
 
 
-subsection "Some lemmas about records";
+subsection {* Some lemmas about records *};
 
-text "Note: any of these goals may be solved with a single
- stroke of auto or force.";
+text {* Note: any of these goals may be solved with a single
+ stroke of the auto or force proof method. *};
 
 
-text "basic simplifications";
+text {* basic simplifications *};
 
 lemma "x (| x = m, y = n, ... = p |) = m";
   by simp;
@@ -73,7 +73,7 @@
   by simp;
 
 
-text "splitting quantifiers: the !!r is NECESSARY";
+text {* splitting quantifiers: the !!r is NECESSARY *};
 
 lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
 proof record_split;
@@ -92,7 +92,7 @@
 qed;
 
 
-text "equality of records";
+text {* equality of records *};
 
 lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
 proof;
@@ -101,14 +101,14 @@
 qed;
 
 
-text "concrete records are type instances of record schemes";
+text {* concrete records are type instances of record schemes *};
 
 constdefs
   foo5 :: nat
   "foo5 == getX (| x = 1, y = 0 |)";
 
 
-text "manipulating the `...' (more) part";
+text {* manipulating the `...' (more) part *};
 
 constdefs
   incX :: "('a::more) point_scheme => 'a point_scheme"
@@ -121,7 +121,7 @@
 qed;
 
 
-text "alternative definition";
+text {* alternative definition *};
 
 constdefs
   incX' :: "('a::more) point_scheme => 'a point_scheme"
@@ -129,7 +129,7 @@
 
 
 
-section "coloured points: record extension";
+section {* coloured points: record extension *};
 
 datatype colour = Red | Green | Blue;
 
@@ -150,16 +150,16 @@
 consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)";
 
 
-text "functions on point schemes work for cpoints as well";
+text {* functions on point schemes work for cpoints as well *};
 
 constdefs
   foo10 :: nat
   "foo10 == getX (| x = 2, y = 0, colour = Blue |)";
 
 
-subsection "Non-coercive structural subtyping";
+subsection {* Non-coercive structural subtyping *};
 
-text "foo11 has type cpoint, not type point --- Great!";
+text {* foo11 has type cpoint, not type point --- Great! *};
 
 constdefs
   foo11 :: cpoint
@@ -167,9 +167,9 @@
 
 
 
-section "Other features";
+section {* Other features *};
 
-text "field names contribute to record identity";
+text {* field names contribute to record identity *};
 
 record point' =
   x' :: nat
@@ -181,7 +181,7 @@
 text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *};
 
 
-text "polymorphic records";
+text {* polymorphic records *};
 
 record 'a point'' = point +
   content :: 'a;
@@ -189,6 +189,6 @@
 types cpoint'' = "colour point''";
 
 
-text "Have a lot of fun!";
+text {* Have a lot of fun! *};
 
 end;