src/HOL/ex/set.thy
changeset 15306 51f3d31e8eea
parent 14353 79f9fbef9106
child 15481 fc075ae929e4
     1.1 --- a/src/HOL/ex/set.thy	Mon Nov 22 11:53:56 2004 +0100
     1.2 +++ b/src/HOL/ex/set.thy	Mon Nov 22 11:54:08 2004 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4    apply (rule bij_if_then_else)
     1.5       apply (rule_tac [4] refl)
     1.6      apply (rule_tac [2] inj_on_inv)
     1.7 -    apply (erule subset_inj_on [OF subset_UNIV])
     1.8 +    apply (erule subset_inj_on [OF _ subset_UNIV])
     1.9     txt {* Tricky variable instantiations! *}
    1.10     apply (erule ssubst, subst double_complement)
    1.11     apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)