tuned;

--- a/src/HOL/Isar_examples/Cantor.thy	Tue Apr 27 10:45:20 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Tue Apr 27 10:46:37 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
@@ -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 {|
   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;
@@ -63,7 +63,7 @@
   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;
@@ -98,7 +98,7 @@
   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);
@@ -109,7 +109,7 @@
   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;

--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Apr 27 10:45:20 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Apr 27 10:46:37 1999 +0200
@@ -101,7 +101,6 @@
   @{term "comp"}.  We first establish some lemmas.
 |};
 
-ML "reset HOL_quantifiers";
 
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");