Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compile
authorblanchet
Mon, 21 Jun 2010 13:35:10 +0200
changeset 37481 bd80d84b904d
parent 37480 d5a85d35ef62
child 37482 6849464ab10e
compile
src/HOL/Nitpick_Examples/Typedef_Nits.thy file | annotate | diff | comparison | revisions 
--- 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]
isabelle