Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added rev_ballE
authoroheimb
Fri, 11 Jul 2003 14:11:56 +0200
changeset 14098 54f130df1136
parent 14097 f4d2ff3cad09
child 14099 55d244f3c86d
added rev_ballE
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle