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.
make proof work again
authorblanchet
Fri, 04 Dec 2009 17:18:07 +0100
changeset 33979 854e12dafd28
parent 33978 2380c1dac86e
child 33980 a28733ef3a82
make proof work again
src/HOL/Nitpick_Examples/Typedef_Nits.thy file | annotate | diff | comparison | revisions 
--- 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