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/ex/set.thy
changeset 15306 51f3d31e8eea
parent 14353 79f9fbef9106
child 15481 fc075ae929e4 
--- a/src/HOL/ex/set.thy	Mon Nov 22 11:53:56 2004 +0100
+++ b/src/HOL/ex/set.thy	Mon Nov 22 11:54:08 2004 +0100
@@ -108,7 +108,7 @@
   apply (rule bij_if_then_else)
      apply (rule_tac [4] refl)
     apply (rule_tac [2] inj_on_inv)
-    apply (erule subset_inj_on [OF subset_UNIV])
+    apply (erule subset_inj_on [OF _ subset_UNIV])
    txt {* Tricky variable instantiations! *}
    apply (erule ssubst, subst double_complement)
    apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
isabelle