| changeset 37481 | bd80d84b904d |
| parent 37478 | d8dd5a4403d2 |
| child 38542 | c9599ce8cbfc |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 21 12:33:43 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 21 13:35:10 2010 +0200 @@ -176,7 +176,7 @@ lemma "make_point_ext_type (dest_point_ext_type a) = a" nitpick [expect = none] -by (rule Rep_point_ext_type_inverse) +by (rule dest_point_ext_type_inverse) lemma "Fract a b = of_int a / of_int b" nitpick [card = 1, expect = none]