author wenzelm Tue, 27 Apr 1999 10:46:37 +0200 changeset 6517 239c0eff6ce8 parent 6516 09207771cc7c child 6518 e9d6f165f9c1
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");