# HG changeset patch # User wenzelm # Date 1329330687 -3600 # Node ID f584616218393b11459e70ede15a31d129aeaa82 # Parent 50fca9d09528bb138e11240261dba68ab7400c43 NEWS; diff -r 50fca9d09528 -r f58461621839 NEWS --- a/NEWS Wed Feb 15 17:49:03 2012 +0100 +++ b/NEWS Wed Feb 15 19:31:27 2012 +0100 @@ -11,6 +11,9 @@ - markup for bound variables - markup for types of term variables (e.g. displayed as tooltips) +* Updated and extended reference manuals ("isar-ref" and +"implementation"); reduced remaining material in old "ref" manual. + * Rule attributes in local theory declarations (e.g. locale or class) are now statically evaluated: the resulting theorem is stored instead of the original expression. INCOMPATIBILITY in rare situations, where