| changeset 60371 | 8a5cfdda1b98 |
| parent 60370 | 9ec1d3d2068e |
| child 60387 | 76359ff1090f |
--- a/NEWS Fri Jun 05 13:26:12 2015 +0200 +++ b/NEWS Fri Jun 05 13:41:06 2015 +0200 @@ -9,6 +9,9 @@ *** Pure *** +* New Isar command 'supply' supports fact definitions during goal +refinement ('apply' scripts). + * Configuration option rule_insts_schematic has been discontinued (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.