src/HOL/Isar_examples/Cantor.thy
 changeset 7982 d534b897ce39 parent 7955 f30e08579481 child 9474 b0ce3b7c9c26
     1.1 --- a/src/HOL/Isar_examples/Cantor.thy	Sat Oct 30 20:13:16 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Sat Oct 30 20:20:48 1999 +0200
1.3 @@ -30,7 +30,7 @@
1.4   with the innermost reasoning expressed quite naively.
1.5  *};
1.6
1.7 -theorem "EX S. S ~: range(f :: 'a => 'a set)";
1.8 +theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.9  proof;
1.10    let ?S = "{x. x ~: f x}";
1.11    show "?S ~: range f";
1.12 @@ -69,7 +69,7 @@
1.13   introduced \emph{before} its corresponding \isacommand{show}.}
1.14  *};
1.15
1.16 -theorem "EX S. S ~: range(f :: 'a => 'a set)";
1.17 +theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.18  proof;
1.19    let ?S = "{x. x ~: f x}";
1.20    show "?S ~: range f";
1.21 @@ -95,22 +95,22 @@
1.22
1.23  text {*
1.24   How much creativity is required?  As it happens, Isabelle can prove
1.25 - this theorem automatically.  The default context of the Isabelle's
1.26 - classical prover contains rules for most of the constructs of HOL's
1.27 - set theory.  We must augment it with \name{equalityCE} to break up
1.28 - set equalities, and then apply best-first search.  Depth-first search
1.29 - would diverge, but best-first search successfully navigates through
1.30 - the large search space.
1.31 + this theorem automatically.  The context of Isabelle's classical
1.32 + prover contains rules for most of the constructs of HOL's set theory.
1.33 + We must augment it with \name{equalityCE} to break up set equalities,
1.34 + and then apply best-first search.  Depth-first search would diverge,
1.35 + but best-first search successfully navigates through the large search
1.36 + space.
1.37  *};
1.38
1.39 -theorem "EX S. S ~: range(f :: 'a => 'a set)";
1.40 +theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.41    by (best elim: equalityCE);
1.42
1.43  text {*
1.44   While this establishes the same theorem internally, we do not get any
1.45   idea of how the proof actually works.  There is currently no way to
1.46   transform internal system-level representations of Isabelle proofs
1.47 - back into Isar documents.  Writing intelligible proof documents
1.48 + back into Isar text.  Writing intelligible proof documents
1.49   really is a creative process, after all.
1.50  *};
1.51