# HG changeset patch
# User wenzelm
# Date 1447426979 -3600
# Node ID 5dce70aecbfca12d8d3b4b638306bb625984789c
# Parent  5b878bc6ae98259c9ec235ab68cdba201a6f0f17
more documentation;

diff -r 5b878bc6ae98 -r 5dce70aecbfc NEWS
--- a/NEWS	Fri Nov 13 15:06:58 2015 +0100
+++ b/NEWS	Fri Nov 13 16:02:59 2015 +0100
@@ -176,6 +176,26 @@
 The keyword 'when' may be used instead of 'if', to indicate 'presume'
 instead of 'assume' above.
 
+* Assumptions ('assume', 'presume') allow structured statements using
+'if' and 'for', similar to 'have' etc. above. For example:
+
+  assume result: "C x y"
+    if "A x" and "B y"
+    for x :: 'a and y :: 'a
+
+This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general
+result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".
+
+Vacuous quantification in assumptions is omitted, i.e. a for-context
+only effects propositions according to actual use of variables. For
+example:
+
+  assume "A x" and "B y" for x and y
+
+is equivalent to:
+
+  assume "\<And>x. A x" and "\<And>y. B y"
+
 * The meaning of 'show' with Pure rule statements has changed: premises
 are treated in the sense of 'assume', instead of 'presume'. This means,
 a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
diff -r 5b878bc6ae98 -r 5dce70aecbfc src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Nov 13 15:06:58 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Nov 13 16:02:59 2015 +0100
@@ -349,6 +349,8 @@
     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     ;
     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
+    ;
+    @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +)
   \<close>}
 
   The treatment of multiple declarations corresponds to the
diff -r 5b878bc6ae98 -r 5dce70aecbfc src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 15:06:58 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 16:02:59 2015 +0100
@@ -160,7 +160,11 @@
   @{rail \<open>
     @@{command fix} @{syntax "fixes"}
     ;
-    (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
+    (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
+    ;
+    concl: (@{syntax props} + @'and')
+    ;
+    prems: (@'if' (@{syntax props'} + @'and'))?
     ;
     @@{command def} (def + @'and')
     ;
@@ -181,6 +185,10 @@
   "and"}; the resulting list of current facts consists of all of these
   concatenated.
 
+  A structured assumption like \<^theory_text>\<open>assume "B x" and "A x" for x\<close> is equivalent
+  to \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
+  for-context only effects propositions according to actual use of variables.
+
   \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
   In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
   ``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command