src/HOL/Set.thy
changeset 31945 d5f186aa0bed
parent 31643 b040f1679f77
child 31991 37390299214a
     1.1 --- a/src/HOL/Set.thy	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -449,7 +449,7 @@
     1.4  lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     1.5    by (unfold Ball_def) blast
     1.6  
     1.7 -ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
     1.8 +ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
     1.9  
    1.10  text {*
    1.11    \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and