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