| changeset 19263 | a86d09815dac |
| parent 19254 | efaf5d47049e |
| child 19277 | f7602e74d948 |
--- a/NEWS Tue Mar 14 16:29:39 2006 +0100 +++ b/NEWS Tue Mar 14 22:06:29 2006 +0100 @@ -122,6 +122,10 @@ resulting rule, for later use with the 'cases' method (cf. attribute case_names). +* Isar: 'print_statement' prints theorems from the current theory or +proof context in long statement form, according to the syntax of a +top-level lemma. + * Isar: 'obtain' takes an optional case name for the local context introduction rule (default "that").