added rev_ballE
authoroheimb
Fri Jul 11 14:11:56 2003 +0200 (2003-07-11)
changeset 1409854f130df1136
parent 14097 f4d2ff3cad09
child 14099 55d244f3c86d
added rev_ballE
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Fri Jul 11 13:54:32 2003 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Jul 11 14:11:56 2003 +0200
     1.3 @@ -247,6 +247,7 @@
     1.4  
     1.5  lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     1.6    by (unfold Ball_def) blast
     1.7 +ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *}
     1.8  
     1.9  text {*
    1.10    \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and