# HG changeset patch
# User paulson
# Date 861610500 -7200
# Node ID 62a5230883bb5dd2b9cb9308586e71dfab20de87
# Parent  86aaab39ebb170db762749a2db100c050f256e19
New blast_tac demo

diff -r 86aaab39ebb1 -r 62a5230883bb src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Mon Apr 21 10:14:31 1997 +0200
+++ b/src/HOL/ex/set.ML	Mon Apr 21 10:15:00 1997 +0200
@@ -9,6 +9,16 @@
 
 writeln"File HOL/ex/set.";
 
+set_current_thy"Set";
+
+(*Nice demonstration of blast_tac--and its overloading problems*)
+goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI
+in    (*Type instantiation is required so that blast_tac can apply equalityI
+        to the subgoal arising from insertCI*)
+by(blast_tac (!claset addSIs [insertCI']) 1)
+end;
+
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
 
 val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";