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";