# HG changeset patch
# User wenzelm
# Date 1164138478 -3600
# Node ID 379f130843f7d67cc3d02ff1d59124fe58eee251
# Parent  3d57db34633bd58884f740cd65348cff6d1a0970
* Isar: the assumptions of a long theorem statement are available as assms;

diff -r 3d57db34633b -r 379f130843f7 NEWS
--- a/NEWS	Tue Nov 21 18:50:54 2006 +0100
+++ b/NEWS	Tue Nov 21 20:47:58 2006 +0100
@@ -218,6 +218,11 @@
 resulting rule, for later use with the 'cases' method (cf. attribute
 case_names).
 
+* Isar: the assumptions of a long theorem statement are available as
+"assms" fact in the proof context.  This is more appropriate than the
+(historical) "prems", which refers to all assumptions of the current
+context, including those from the target locale, proof body etc.
+
 * 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.
diff -r 3d57db34633b -r 379f130843f7 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Nov 21 18:50:54 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Nov 21 20:47:58 2006 +0100
@@ -892,13 +892,14 @@
 Claims at the theory level may be either in short or long form.  A
 short goal merely consists of several simultaneous propositions (often
 just one).  A long goal includes an explicit context specification for
-the subsequent conclusion, involving local parameters.  Here the role
-of each part of the statement is explicitly marked by separate
-keywords (see also \S\ref{sec:locale}).
-\indexisarelem{shows}\indexisarelem{obtains}Moreover, there are two
-kinds of conclusions: $\isarkeyword{shows}$ states several
-simultaneous propositions (essentially a big conjunction), while
-$\isarkeyword{obtains}$ claims several simultaneous simultaneous
+the subsequent conclusion, involving local parameters and assumptions.
+Here the role of each part of the statement is explicitly marked by
+separate keywords (see also \S\ref{sec:locale}); the local assumptions
+being introduced here are available as $assms$\indexisarthm{assms} in
+the proof.  \indexisarelem{shows}\indexisarelem{obtains}Moreover,
+there are two kinds of conclusions: $\isarkeyword{shows}$ states
+several simultaneous propositions (essentially a big conjunction),
+while $\isarkeyword{obtains}$ claims several simultaneous simultaneous
 contexts of (essentially a big disjunction of eliminated parameters
 and assumptions, cf.\ \S\ref{sec:obtain}).