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.
deactivated »unknown« nitpick example
authorhaftmann
Sat, 20 Aug 2011 09:42:12 +0200
changeset 44328 cbc6187710c9
parent 44327 46d5e7f52ba5
child 44329 6325ea1c5dfd
deactivated »unknown« nitpick example
src/HOL/Nitpick_Examples/Typedef_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Aug 20 09:30:23 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Aug 20 09:42:12 2011 +0200
@@ -159,7 +159,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
+(*nitpick [card = 1, unary_ints, max_potential = 0, expect = none] (?)*)
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"
isabelle