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 33979 854e12dafd28
parent 33737 e441fede163d
child 34083 652719832159 
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Dec 04 17:17:52 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Dec 04 17:18:07 2009 +0100
@@ -126,7 +126,7 @@
 
 lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
 nitpick [card = 1, expect = none]
-by (rule Inl_def)
+by (simp only: Inl_def o_def)
 
 lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inr_Rep a)"
 nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
isabelle