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 MHonArc.