# HG changeset patch
# User wenzelm
# Date 924881687 -7200
# Node ID e1e40aa2c2274a40d86dac4ce8ba55797ab82225
# Parent  2863855a69029ddb261d9385549cbbbd5d8374f3
tuned;

diff -r 2863855a6902 -r e1e40aa2c227 src/HOL/Isar_examples/Cantor.thy
--- 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;