NEWS
changeset 21447 379f130843f7
parent 21406 4058f0886448
child 21462 74ddf3a522f8
     1.1 --- a/NEWS	Tue Nov 21 18:50:54 2006 +0100
     1.2 +++ b/NEWS	Tue Nov 21 20:47:58 2006 +0100
     1.3 @@ -218,6 +218,11 @@
     1.4  resulting rule, for later use with the 'cases' method (cf. attribute
     1.5  case_names).
     1.6  
     1.7 +* Isar: the assumptions of a long theorem statement are available as
     1.8 +"assms" fact in the proof context.  This is more appropriate than the
     1.9 +(historical) "prems", which refers to all assumptions of the current
    1.10 +context, including those from the target locale, proof body etc.
    1.11 +
    1.12  * Isar: 'print_statement' prints theorems from the current theory or
    1.13  proof context in long statement form, according to the syntax of a
    1.14  top-level lemma.