# HG changeset patch
# User wenzelm
# Date 924882467 -7200
# Node ID 644d75d0dc8cdd3a6f1c2fc5e673965cd7d81eae
# Parent  e1e40aa2c2274a40d86dac4ce8ba55797ab82225
tuned;

diff -r e1e40aa2c227 -r 644d75d0dc8c src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Fri Apr 23 17:34:47 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Fri Apr 23 17:47:47 1999 +0200
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Cantor's theorem -- Isar'ized version of the final section of the HOL
-chapter of 'Isabelle's Object-Logics' (by Larry Paulson).
+chapter of "Isabelle's Object-Logics" (Larry Paulson).
 *)
 
 theory Cantor = Main:;
@@ -108,7 +108,7 @@
   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.
+  documents actually \emph{is} a creative process.
 |}