author  wenzelm 
Fri, 16 Apr 1999 17:44:29 +0200  
changeset 6444  2ebe9e630cab 
child 6494  ab1442d2e4e1 
permissions  rwrr 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Isar_examples/Cantor.thy 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

4 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

5 
Cantor's theorem (see also 'Isabelle's ObjectLogics'). 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

6 
*) 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

7 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

8 
theory Cantor = Main:; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

9 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

10 
theorem cantor: "EX S. S ~: range(f :: 'a => 'a set)"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

11 
by (best elim: equalityCE); 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

12 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

13 
end; 