[isabelle-dev] NEWS

Makarius makarius at sketis.net
Wed Mar 5 21:53:01 CET 2008


* Indexing of literal facts: be more serious about including only
facts from the visible specification/proof context, but not the
background context (locale etc.).  Affects `prop` notation and method
"fact".  INCOMPATIBILITY: need to name facts explicitly in rare
situations.


More information about the isabelle-dev mailing list