| changeset 14098 | 54f130df1136 |
| parent 13865 | 0a6bf71955b0 |
| child 14208 | 144f45277d5a |
--- a/src/HOL/Set.thy Fri Jul 11 13:54:32 2003 +0200 +++ b/src/HOL/Set.thy Fri Jul 11 14:11:56 2003 +0200 @@ -247,6 +247,7 @@ lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" by (unfold Ball_def) blast +ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *} text {* \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and