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