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.
tuned op
authornipkow
Sat, 06 Jan 2018 15:08:42 +0100
changeset 67346 1f1d85393d70
parent 67345 debef21cbed6
child 67347 bf269672c203
child 67352 5f7f339f3d7e
tuned op
src/HOL/Nitpick_Examples/Manual_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 06 13:05:25 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 06 15:08:42 2018 +0100
@@ -81,7 +81,7 @@
 nitpick [expect = none]
 oops
 
-lemma "P (op +::nat\<Rightarrow>nat\<Rightarrow>nat)"
+lemma "P ((op +)::nat\<Rightarrow>nat\<Rightarrow>nat)"
 nitpick [card nat = 1, expect = genuine]
 nitpick [card nat = 2, expect = none]
 oops
isabelle