Re: [isabelle] lemmas-command normalizes theorems
On Fri, 11 Jul 2014, Peter Lammich wrote:
I stumbled over the following (unexpected, undocumented) behaviour of
the lemmas command:
I am surprised that the normal Isabelle rule normalization is unexpected.
It is documented in many places, e.g. the "implementation" manual section
2.4 Object-level rules.
Is there a way, other than raw isabelle-ML declaration, to avoid this
normalization and just give a name to a list of theorems?
There are some tricks with the "prop" marker to protect Pure propositions
(covered in the same manual). This is for unusual situations where this
is really needed.
Normally it is better to work with the system and its canonical rule
format, not against it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and