# HG changeset patch
# User wenzelm
# Date 1469024290 -7200
# Node ID 58980a8b2faff857c5d6feb4885b2549c8c853ac
# Parent  0f39f59317c15f198fb8dc767cf87de9de65fc9e
oops;

diff -r 0f39f59317c1 -r 58980a8b2faf src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Jul 20 16:02:00 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Jul 20 16:18:10 2016 +0200
@@ -189,8 +189,8 @@
   "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
+  A structured assumption like \<^theory_text>\<open>assume "B x" if "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> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.