src/HOL/ex/set.thy
changeset 32988 d1d4d7a08a66
parent 24853 aab5798e5a33
child 33057 764547b68538
     1.1 --- a/src/HOL/ex/set.thy	Sat Oct 17 13:46:55 2009 +0200
     1.2 +++ b/src/HOL/ex/set.thy	Sun Oct 18 12:07:25 2009 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4      --{*The term above can be synthesized by a sufficiently detailed proof.*}
     1.5    apply (rule bij_if_then_else)
     1.6       apply (rule_tac [4] refl)
     1.7 -    apply (rule_tac [2] inj_on_inv)
     1.8 +    apply (rule_tac [2] inj_on_inv_onto)
     1.9      apply (erule subset_inj_on [OF _ subset_UNIV])
    1.10     apply blast
    1.11    apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])