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.

     2.1 --- a/doc-src/IsarRef/pure.tex	Tue Nov 21 18:50:54 2006 +0100
     2.2 +++ b/doc-src/IsarRef/pure.tex	Tue Nov 21 20:47:58 2006 +0100
     2.3 @@ -892,13 +892,14 @@
     2.4  Claims at the theory level may be either in short or long form.  A
     2.5  short goal merely consists of several simultaneous propositions (often
     2.6  just one).  A long goal includes an explicit context specification for
     2.7 -the subsequent conclusion, involving local parameters.  Here the role
     2.8 -of each part of the statement is explicitly marked by separate
     2.9 -keywords (see also \S\ref{sec:locale}).
    2.10 -\indexisarelem{shows}\indexisarelem{obtains}Moreover, there are two
    2.11 -kinds of conclusions: $\isarkeyword{shows}$ states several
    2.12 -simultaneous propositions (essentially a big conjunction), while
    2.13 -$\isarkeyword{obtains}$ claims several simultaneous simultaneous
    2.14 +the subsequent conclusion, involving local parameters and assumptions.
    2.15 +Here the role of each part of the statement is explicitly marked by
    2.16 +separate keywords (see also \S\ref{sec:locale}); the local assumptions
    2.17 +being introduced here are available as $assms$\indexisarthm{assms} in
    2.18 +the proof.  \indexisarelem{shows}\indexisarelem{obtains}Moreover,
    2.19 +there are two kinds of conclusions: $\isarkeyword{shows}$ states
    2.20 +several simultaneous propositions (essentially a big conjunction),
    2.21 +while $\isarkeyword{obtains}$ claims several simultaneous simultaneous
    2.22  contexts of (essentially a big disjunction of eliminated parameters
    2.23  and assumptions, cf.\ \S\ref{sec:obtain}).
    2.24