author | haftmann |
Wed, 18 Aug 2010 16:59:36 +0200 | |
changeset 38542 | c9599ce8cbfc |
parent 38541 | 9cfafdb56749 |
child 38543 | 6a65b92edf5e |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Aug 18 16:59:36 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Aug 18 16:59:36 2010 +0200 @@ -174,9 +174,9 @@ Xcoord :: int Ycoord :: int -lemma "make_point_ext_type (dest_point_ext_type a) = a" +lemma "Abs_point_ext (Rep_point_ext a) = a" nitpick [expect = none] -by (rule dest_point_ext_type_inverse) +by (fact Rep_point_ext_inverse) lemma "Fract a b = of_int a / of_int b" nitpick [card = 1, expect = none]