src/HOL/Set.thy
changeset 14098 54f130df1136
parent 13865 0a6bf71955b0
child 14208 144f45277d5a
     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