# HG changeset patch
# User paulson
# Date 861610601 -7200
# Node ID 7ecb8b6a3d7fefbca975f899c1de58923bf349af
# Parent  fad7cc42624274892526c7b017d9d13e9db35fd1
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML

diff -r fad7cc426242 -r 7ecb8b6a3d7f src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Mon Apr 21 10:16:01 1997 +0200
+++ b/src/ZF/ex/misc.ML	Mon Apr 21 10:16:41 1997 +0200
@@ -9,6 +9,11 @@
 
 writeln"ZF/ex/misc";
 
+(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
+goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+by (Blast_tac 1);
+result();
+
 set_current_thy"Perm";
 
 (*Example 12 (credited to Peter Andrews) from
diff -r fad7cc426242 -r 7ecb8b6a3d7f src/ZF/func.ML
--- a/src/ZF/func.ML	Mon Apr 21 10:16:01 1997 +0200
+++ b/src/ZF/func.ML	Mon Apr 21 10:16:41 1997 +0200
@@ -310,11 +310,6 @@
 	(*by (Blast_tac 1);  takes too long...*)
 qed "function_Union";
 
-(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
-goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
-by (Blast_tac 1);
-result();
-
 goalw ZF.thy [Pi_def]
     "!!S. [| ALL f:S. EX C D. f:C->D; \
 \            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \