changeset 33057 | 764547b68538 |
parent 32988 | d1d4d7a08a66 |
child 34055 | fdf294ee08b2 |
--- a/src/HOL/ex/set.thy Wed Oct 21 17:34:35 2009 +0200 +++ b/src/HOL/ex/set.thy Thu Oct 22 09:27:48 2009 +0200 @@ -104,7 +104,7 @@ --{*The term above can be synthesized by a sufficiently detailed proof.*} apply (rule bij_if_then_else) apply (rule_tac [4] refl) - apply (rule_tac [2] inj_on_inv_onto) + apply (rule_tac [2] inj_on_inv_into) apply (erule subset_inj_on [OF _ subset_UNIV]) apply blast apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])