Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Typedef_Nits.thy
changeset 40590 b994d855dbd2
parent 40341 03156257040f
child 41278 8e1cde88aae6 
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 13:37:17 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 16:36:57 2010 -0800
@@ -89,7 +89,7 @@
 
 lemma "Rep_unit () = True"
 nitpick [expect = none]
-by (insert Rep_unit) (simp add: unit_def)
+by (insert Rep_unit) simp
 
 lemma "Rep_unit () = False"
 nitpick [expect = genuine]
isabelle