[isabelle-dev] NEWS

Clemens Ballarin ballarin at in.tum.de
Wed Jul 25 10:18:07 CEST 2007

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


More information about the isabelle-dev mailing list