# HG changeset patch
# User wenzelm
# Date 957812329 -7200
# Node ID 31da5b9790c00b39112489bd1fe5166269a98897
# Parent  4eaa99f0d22395263fc95f6cb3a785a295a147ed
strip = impI allI allI;

diff -r 4eaa99f0d223 -r 31da5b9790c0 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Mon May 08 20:57:02 2000 +0200
+++ b/src/HOL/Set.ML	Mon May 08 20:58:49 2000 +0200
@@ -44,6 +44,8 @@
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "ballI";
 
+bind_thms ("strip", [impI, allI, ballI]);
+
 Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
 by (Blast_tac 1);
 qed "bspec";