| changeset 67346 | 1f1d85393d70 |
| parent 66453 | cc19f7ca2ed6 |
| child 67399 | eab6ce8368fa |
| 67345:debef21cbed6 | 67346:1f1d85393d70 |
|---|---|
79 |
79 |
80 lemma "P Suc" |
80 lemma "P Suc" |
81 nitpick [expect = none] |
81 nitpick [expect = none] |
82 oops |
82 oops |
83 |
83 |
84 lemma "P (op +::nat\<Rightarrow>nat\<Rightarrow>nat)" |
84 lemma "P ((op +)::nat\<Rightarrow>nat\<Rightarrow>nat)" |
85 nitpick [card nat = 1, expect = genuine] |
85 nitpick [card nat = 1, expect = genuine] |
86 nitpick [card nat = 2, expect = none] |
86 nitpick [card nat = 2, expect = none] |
87 oops |
87 oops |
88 |
88 |
89 |
89 |