--- 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;
--- 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
--- 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);
--- 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);
--- 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;
--- 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;