# HG changeset patch
# User wenzelm
# Date 1465657097 -7200
# Node ID ce90bb3d29025fbaa66d584dd4be20f10421e970
# Parent  e9c777bfd78ccb6b82e21c7386db724222b1fefb
clarified;

diff -r e9c777bfd78c -r ce90bb3d2902 src/Doc/Isar_Ref/Quick_Reference.thy
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 16:41:11 2016 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 16:58:17 2016 +0200
@@ -13,17 +13,20 @@
 text \<open>
   \begin{tabular}{rcl}
     \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if props for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+    & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
     \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\
     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>subgoal "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>subgoal for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\
     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
@@ -32,12 +35,9 @@
     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<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 vars "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>show name: props "proof"\<close> \\
+    \<open>goal\<close> & = & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
   \end{tabular}
 \<close>