proper syntax; Isabelle2016
authorwenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 62283 f005a691df1f
child 62338 ec44535f954a
proper syntax;
src/Doc/Isar_Ref/Quick_Reference.thy
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Fri Feb 12 17:04:36 2016 +0100
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Mon Feb 15 14:55:44 2016 +0100
@@ -33,7 +33,7 @@
     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>fix "var\<^sup>+"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if name: props for "var\<^sup>+"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for "var\<^sup>+"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
     \<open>goal\<close> & = & \<^theory_text>\<open>have name: props "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for "var\<^sup>+" "proof"\<close> \\