--- a/src/HOL/Isar_examples/Cantor.thy Fri Apr 23 17:02:10 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Fri Apr 23 17:34:47 1999 +0200
@@ -25,6 +25,7 @@
@{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
@@ -57,6 +58,7 @@
qed;
qed;
+
text {|
The following version essentially does the same reasoning, only that
it is expressed more neatly, with some derived Isar language
@@ -103,10 +105,11 @@
text {|
While this establishes the same theorem internally, we do not get
- any idea of how the actually works. There is currently no way to
- transform internal system-level representations of proofs back into
- Isar documents. Writing Isabelle/Isar proof documents actually
- \emph{is} an creative process.
+ 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} an creative process.
|}
+
end;