| changeset 60489 | bfd9b7302a82 |
| parent 60479 | db238135f386 |
| child 60497 | 010c26e24c72 |
--- a/NEWS Mon Jun 15 16:24:52 2015 +0200 +++ b/NEWS Mon Jun 15 16:59:27 2015 +0200 @@ -65,6 +65,9 @@ *** Pure *** +* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` +as well, not just "by this" or "." as before. + * Configuration option rule_insts_schematic has been discontinued (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.