strip = impI allI allI;
authorwenzelm
Mon May 08 20:58:49 2000 +0200 (2000-05-08)
changeset 883931da5b9790c0
parent 8838 4eaa99f0d223
child 8840 18b76c137c41
strip = impI allI allI;
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Mon May 08 20:57:02 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon May 08 20:58:49 2000 +0200
     1.3 @@ -44,6 +44,8 @@
     1.4  by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
     1.5  qed "ballI";
     1.6  
     1.7 +bind_thms ("strip", [impI, allI, ballI]);
     1.8 +
     1.9  Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
    1.10  by (Blast_tac 1);
    1.11  qed "bspec";