# HG changeset patch
# User wenzelm
# Date 925202720 -7200
# Node ID 09207771cc7c6fa0a405bdfe50bea6d8e97f1e0c
# Parent  18e113be12eeb37259213a1530bcba0dff787abd
added Isar_examples/Cantor.ML;

diff -r 18e113be12ee -r 09207771cc7c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Apr 27 10:44:42 1999 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 27 10:45:20 1999 +0200
@@ -325,8 +325,9 @@
 HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
 
 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
-  Isar_examples/Cantor.thy Isar_examples/ExprCompiler.thy \
-  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
+  Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
+  Isar_examples/ExprCompiler.thy Isar_examples/Peirce.thy \
+  Isar_examples/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
 
 
diff -r 18e113be12ee -r 09207771cc7c src/HOL/Isar_examples/Cantor.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Cantor.ML	Tue Apr 27 10:45:20 1999 +0200
@@ -0,0 +1,20 @@
+
+(* tactic script -- single steps *)
+
+Goal "EX S. S ~: range(f :: 'a => 'a set)";
+  br exI 1;
+  br notI 1;
+  be rangeE 1;
+  be equalityCE 1;
+  bd CollectD 1;
+  by (contr_tac 1);
+  by (swap_res_tac [CollectI] 1);
+  ba 1;
+qed "it";
+
+
+(* tactic script -- automatic *)
+
+Goal "EX S. S ~: range(f :: 'a => 'a set)";
+  by (best_tac (claset() addSEs [equalityCE]) 1);
+qed "it";