--- a/src/HOL/Isar_Examples/Cantor.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,14 +8,11 @@
imports Main
begin
-text_raw {*
- \footnote{This is an Isar version of the final example of the
- Isabelle/HOL manual \cite{isabelle-HOL}.}
-*}
+text_raw {* \footnote{This is an Isar version of the final example of
+ the Isabelle/HOL manual \cite{isabelle-HOL}.} *}
-text {*
- Cantor's Theorem states that every set has more subsets than it has
- elements. It has become a favorite basic example in pure
+text {* Cantor's Theorem states that every set has more subsets than
+ it has elements. It has become a favorite basic example in pure
higher-order logic since it is so easily expressed: \[\all{f::\alpha
\To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
\all{x::\alpha} f \ap x \not= S\]
@@ -25,8 +22,7 @@
every function from $\alpha$ to its powerset, some subset is outside
its range. The Isabelle/Isar proofs below uses HOL's set theory,
with the type $\alpha \ap \idt{set}$ and the operator
- $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
-*}
+ $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
theorem "EX S. S ~: range (f :: 'a => 'a set)"
proof
@@ -48,24 +44,20 @@
qed
qed
-text {*
- How much creativity is required? As it happens, Isabelle can prove
- this theorem automatically using best-first search. Depth-first
- search would diverge, but best-first search successfully navigates
- through the large search space. The context of Isabelle's classical
- prover contains rules for the relevant constructs of HOL's set
- theory.
-*}
+text {* How much creativity is required? As it happens, Isabelle can
+ prove this theorem automatically using best-first search.
+ Depth-first search would diverge, but best-first search successfully
+ navigates through the large search space. The context of Isabelle's
+ classical prover contains rules for the relevant constructs of HOL's
+ set theory. *}
theorem "EX S. S ~: range (f :: 'a => 'a set)"
by best
-text {*
- While this establishes the same theorem internally, we do not get
- any idea of how the proof actually works. There is currently no way
- to transform internal system-level representations of Isabelle
+text {* While this establishes the same theorem internally, we do not
+ get 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 text. Writing intelligible proof documents
- really is a creative process, after all.
-*}
+ really is a creative process, after all. *}
end