changeset 37478 | d8dd5a4403d2 |
parent 37400 | cf5e06d5ecaf |
child 37481 | bd80d84b904d |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 21 11:16:00 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 21 12:28:46 2010 +0200 @@ -174,7 +174,7 @@ Xcoord :: int Ycoord :: int -lemma "Abs_point_ext_type (Rep_point_ext_type a) = a" +lemma "make_point_ext_type (dest_point_ext_type a) = a" nitpick [expect = none] by (rule Rep_point_ext_type_inverse)