| changeset 27381 | 19ae7064f00f |
| parent 27380 | ca505e7b7591 |
| child 27391 | 6c4649134fd6 |
--- a/NEWS Sat Jun 28 15:30:46 2008 +0200 +++ b/NEWS Sat Jun 28 21:21:13 2008 +0200 @@ -19,6 +19,12 @@ interface instead. +*** Document preparation *** + +* Antiquotation @{lemma} now imitates a regular terminal proof, +demanding keyword 'by' and supporting the full method expressions. + + *** HOL *** * Methods "case_tac" and "induct_tac" now refer to the very same rules