[isabelle] mono attribute
I'm a bit confused about the [mono] attribute. The Isar tutorial says that I can declare new monotonicity rules using the mono attribute, but when I type the simplest monotonicity lemma I can think of:
lemma blah [mono]:
"x ≤ y ⟹ Suc x ≤ Suc y"
I get the following error:
Bad monotonicity theorem:
?x ≤ ?y ⟹ Suc ?x ≤ Suc ?y
Could somebody kindly explain what's happening here? Thanks very much.
This archive was generated by a fusion of
Pipermail (Mailman edition) and