Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/ELT.thy
changeset 45605 a89b4bc311a5
parent 44106 0e018cbcc0de
child 46577 e5438c5797ae 
--- a/src/HOL/UNITY/ELT.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/ELT.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -418,7 +418,7 @@
 apply (blast intro: subset_imp_leadsETo)
 done
 
-lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
+lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
 
 lemma LeadsETo_weaken_R [rule_format]:
      "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
isabelle