# HG changeset patch
# User paulson
# Date 909046730 -7200
# Node ID a9f8cb9b5b5d44cbbdbffafaab92f6fb8bc78223
# Parent  81e1a83ee00265e48838f1b1d8ec7e5fb100e156
standard Blast_tac demos

diff -r 81e1a83ee002 -r a9f8cb9b5b5d src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Thu Oct 22 10:58:18 1998 +0200
+++ b/src/HOL/ex/set.ML	Thu Oct 22 10:58:50 1998 +0200
@@ -16,13 +16,25 @@
 by (Blast_tac 1);
 result();
 
-(*Nice demonstration of blast_tac--and its limitations*)
+(** Examples for the Blast_tac paper **)
+
+(*Union-image, called Un_Union_image on equalities.ML*)
+Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
+by (Blast_tac 1);
+result();
+
+(*Inter-image, called Int_Inter_image on equalities.ML*)
+Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+by (Blast_tac 1);
+result();
+
+(*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
 (*for some unfathomable reason, UNIV_I increases the search space greatly*)
 by (blast_tac (claset() delrules [UNIV_I]) 1);
 result();
 
-(*variant of the benchmark above*)
+(*Singleton II.  variant of the benchmark above*)
 Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
 by (blast_tac (claset() delrules [UNIV_I]) 1);
 (*just Blast_tac takes 5 seconds instead of 1*)