# HG changeset patch
# User wenzelm
# Date 927830950 -7200
# Node ID 9727e83f0578ee6e60a141888eeec8502c0f5944
# Parent  5d50225637c8b01c5095f68ec406f09ab0e55e58
changed {| |} verbatim syntax to {* *};

diff -r 5d50225637c8 -r 9727e83f0578 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Thu May 27 20:47:30 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Thu May 27 20:49:10 1999 +0200
@@ -11,7 +11,7 @@
 
 section "Example: Cantor's Theorem";
 
-text {|
+text {*
   Cantor's Theorem states that every set has more subsets than it has
   elements.  It has become a favourite example in higher-order logic
   since it is so easily expressed: @{display term[show_types] "ALL f
@@ -23,14 +23,14 @@
 
   The Isabelle/Isar proofs below use HOL's set theory, with the type
   @{type "'a set"} and the operator @{term range}.
-|};
+*};
 
 
-text {|
+text {*
   We first consider a rather verbose version of the proof, with the
   reasoning expressed quite naively.  We only make use of the pure
   core of the Isar proof language.
-|};
+*};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
@@ -59,11 +59,11 @@
 qed;
 
 
-text {|
+text {*
   The following version essentially does the same reasoning, only that
   it is expressed more neatly, with some derived Isar language
   elements involved.
-|};
+*};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
@@ -90,7 +90,7 @@
 qed;
 
 
-text {|
+text {*
   How much creativity is required?  As it happens, Isabelle can prove
   this theorem automatically.  The default classical set contains
   rules for most of the constructs of HOL's set theory.  We must
@@ -98,18 +98,18 @@
   then apply best-first search.  Depth-first search would diverge, but
   best-first search successfully navigates through the large search
   space.
-|};
+*};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
   by (best elim: equalityCE);
 
-text {|
+text {*
   While this establishes the same theorem internally, we do not get
   any idea of how the proof actually works.  There is currently no way
   to transform internal system-level representations of Isabelle
   proofs back into Isar documents.  Writing Isabelle/Isar proof
   documents actually \emph{is} a creative process.
-|};
+*};
 
 
 end;
diff -r 5d50225637c8 -r 9727e83f0578 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Thu May 27 20:47:30 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Thu May 27 20:49:10 1999 +0200
@@ -14,10 +14,10 @@
 
 section "Basics";
 
-text {|
+text {*
   First we define a type abbreviation for binary operations over some
   type @{type "'val"} of values.
-|};
+*};
 
 types
   'val binop = "'val => 'val => 'val";
@@ -25,19 +25,19 @@
 
 section "Machine";
 
-text {|
+text {*
   Next we model a simple stack machine, with three instructions.
-|};
+*};
 
 datatype ('adr, 'val) instr =
   Const 'val |
   Load 'adr |
   Apply "'val binop";
 
-text {|
+text {*
   Execution of a list of stack machine instructions is
   straight-forward.
-|};
+*};
 
 consts
   exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
@@ -57,19 +57,19 @@
 
 section "Expressions";
 
-text {|
+text {*
   We introduce a simple language of expressions: variables ---
   constants --- binary operations.
-|};
+*};
 
 datatype ('adr, 'val) expr =
   Variable 'adr |
   Constant 'val |
   Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
 
-text {|
+text {*
   Evaluation of expressions does not do any unexpected things.
-|};
+*};
 
 consts
   eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
@@ -82,10 +82,10 @@
 
 section "Compiler";
 
-text {|
+text {*
   So we are ready to define the compilation function of expressions to
   lists of stack machine instructions.
-|};
+*};
 
 consts
   comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
@@ -96,10 +96,10 @@
   "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
 
 
-text {|
+text {*
   The main result of this developement is the correctness theorem for
   @{term "comp"}.  We first establish some lemmas.
-|};
+*};
 
 
 lemma exec_append:
diff -r 5d50225637c8 -r 9727e83f0578 src/HOL/ex/Points.thy
--- a/src/HOL/ex/Points.thy	Thu May 27 20:47:30 1999 +0200
+++ b/src/HOL/ex/Points.thy	Thu May 27 20:49:10 1999 +0200
@@ -15,7 +15,7 @@
   x :: nat
   y :: nat;
 
-text {|
+text {*
   Apart many other things, above record declaration produces the
   following theorems:
 
@@ -25,16 +25,16 @@
 
   The set of theorems "point.simps" is added automatically to the
   standard simpset, "point.iffs" is added to the claset and simpset.
-|};
+*};
 
-text {|
+text {*
   Record declarations define new type abbreviations:
 
     point = "(| x :: nat, y :: nat |)"
     'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
 
   Extensions `...' must be in type class `more'!
-|};
+*};
 
 consts foo1 :: point;
 consts foo2 :: "(| x :: nat, y :: nat |)";
@@ -137,12 +137,12 @@
   colour :: colour;
 
 
-text {|
+text {*
   The record declaration defines new type constructors:
 
     cpoint = (| x :: nat, y :: nat, colour :: colour |)
     'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
-|};
+*};
 
 consts foo6 :: cpoint;
 consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)";
@@ -178,7 +178,7 @@
 consts
   foo12 :: nat;
 
-text {| Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid |};
+text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *};
 
 
 text "polymorphic records";