[isabelle-dev] NEWS

Makarius makarius at sketis.net
Tue Sep 2 20:05:18 CEST 2008


* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
formalized as type Name.binding, replacing old bstring.
INCOMPATIBILITY, need to wrap strings via Name.binding function, see
also Name.name_of.  Packages should pass name bindings given by the
user to underlying specification mechanisms; this enables precise
tracking of source positions, for example.




More information about the isabelle-dev mailing list