# HG changeset patch
# User eberlm
# Date 1465911314 -7200
# Node ID e7920a0abf4a271ea2a46ce83e636c42ec19a44b
# Parent  71805faedeb2b305cdc53e028fe2d46dd1555968# Parent  70d144cead250bb0c6b0d43b216f3acaa843a0a8
Merged

diff -r 71805faedeb2 -r e7920a0abf4a src/Doc/Isar_Ref/Quick_Reference.thy
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jun 14 13:14:11 2016 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jun 14 15:35:14 2016 +0200
@@ -22,13 +22,13 @@
     & & \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>*" main_proof\<close> \\
+    \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proper_proof\<close> \\
     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
-    \<open>main_proof\<close> & = & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
+    \<open>proper_proof\<close> & = & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>done\<close> \\
     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\