author wenzelm Tue, 21 Nov 2006 20:47:58 +0100 changeset 21447 379f130843f7 parent 21446 3d57db34633b child 21448 09c953c07008
* Isar: the assumptions of a long theorem statement are available as assms;
 NEWS file | annotate | diff | comparison | revisions doc-src/IsarRef/pure.tex file | annotate | diff | comparison | revisions
--- 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.
--- 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
-\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
+being introduced here are available as $assms$\indexisarthm{assms} in
+there are two kinds of conclusions: $\isarkeyword{shows}$ states
+while $\isarkeyword{obtains}$ claims several simultaneous simultaneous