[isabelle-dev] NEWS

[Clemens Ballarin]

* Isar/locales: interpretation in theories and proof contexts has been
extended.  One may now specify (and prove) equations, which are
unfolded in interpreted theorems.  This is useful for replacing
defined concepts (constants depending on locale parameters) by
concepts already existing in the target context.  Example:

   interpretation partial_order ["op <= :: [int, int] => bool"]
     where "partial_order.less (op <=) (x::int) y = (x < y)"

Typically, the constant `partial_order.less' is created by a definition
specification element in the context of locale partial_order.

Clemens