| changeset 67399 | eab6ce8368fa |
| parent 67346 | 1f1d85393d70 |
| child 67414 | c46b3f9f79ea |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Jan 10 15:25:09 2018 +0100 @@ -81,7 +81,7 @@ nitpick [expect = none] oops -lemma "P ((op +)::nat\<Rightarrow>nat\<Rightarrow>nat)" +lemma "P ((+)::nat\<Rightarrow>nat\<Rightarrow>nat)" nitpick [card nat = 1, expect = genuine] nitpick [card nat = 2, expect = none] oops