adjusted to restored naming convention of logical record types
authorhaftmann
Wed, 18 Aug 2010 16:59:36 +0200
changeset 38542 c9599ce8cbfc
parent 38541 9cfafdb56749
child 38543 6a65b92edf5e
adjusted to restored naming convention of logical record types
src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- 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]