| changeset 59660 | 49e498cedd02 |
| parent 59648 | d1148f0baef5 |
| child 59661 | c3b76f2bafbd |
--- a/NEWS Mon Mar 09 11:32:32 2015 +0100 +++ b/NEWS Mon Mar 09 20:33:33 2015 +0100 @@ -6,6 +6,9 @@ *** General *** +* Structural composition of proof methods (meth1; meth2) in Isar +corresponds to (tac1 THEN_ALL_NEW tac2) in ML. + * Generated schematic variables in standard format of exported facts are incremented to avoid material in the proof context. Rare INCOMPATIBILITY, explicit instantiation sometimes needs to refer to