| changeset 59661 | c3b76f2bafbd |
| parent 59659 | 1ce77bca58f8 |
| parent 59660 | 49e498cedd02 |
| child 59675 | 55eb8932d539 |
| child 59730 | b7c394c7a619 |
--- a/NEWS Mon Mar 09 16:42:18 2015 +0000 +++ b/NEWS Mon Mar 09 21:30:42 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