author | blanchet |
Mon, 21 Jun 2010 12:28:46 +0200 | |
changeset 37478 | d8dd5a4403d2 |
parent 37477 | e482320bcbfe |
child 37479 | f6b1ee5b420b |
--- 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)