| changeset 61520 | 8f85bb443d33 |
| parent 60530 | 44f9873d6f6f |
| child 63167 | 0909deb8059b |
--- a/src/HOL/Induct/QuoDataType.thy Mon Oct 26 23:42:01 2015 +0000 +++ b/src/HOL/Induct/QuoDataType.thy Tue Oct 27 15:17:02 2015 +0000 @@ -168,7 +168,7 @@ done text\<open>Reduces equality on abstractions to equality on representatives\<close> -declare inj_on_Abs_Msg [THEN inj_on_iff, simp] +declare inj_on_Abs_Msg [THEN inj_on_eq_iff, simp] declare Abs_Msg_inverse [simp]