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.
reintroduced example now that it's no longer broken
authorblanchet
Fri, 11 May 2012 01:02:36 +0200
changeset 47910 ca5b629a5995
parent 47909 5f1afeebafbc
child 47911 2168126446bb
reintroduced example now that it's no longer broken
src/HOL/Nitpick_Examples/Typedef_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri May 11 00:45:24 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri May 11 01:02:36 2012 +0200
@@ -176,9 +176,7 @@
 by (fact Rep_point_ext_inverse)
 
 lemma "Fract a b = of_int a / of_int b"
-(* FIXME: broken by conversion of Rat.thy to lift_definition/transfer.
 nitpick [card = 1, expect = none]
-*)
 by (rule Fract_of_int_quotient)
 
 lemma "Abs_rat (Rep_rat a) = a"
isabelle