src/Doc/Isar_Ref/Quick_Reference.thy
changeset 63293 9adfdaee327e
parent 63292 5a1f5fc10bb0
child 63298 70d144cead25
equal deleted inserted replaced
63292:5a1f5fc10bb0 63293:9adfdaee327e
    20     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
    20     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
    21     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
    21     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
    22     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
    22     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
    23     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
    23     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
    24     & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
    24     & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
    25     \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
    25     \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" main_proof\<close> \\
    26     & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\
       
    27     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
    26     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
    28     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
    27     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
    29     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
    28     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
    30     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
    29     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
    31     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
    30     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
       
    31     \<open>main_proof\<close> & = & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
       
    32     & \<open>|\<close> & \<^theory_text>\<open>done\<close> \\
    32     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
    33     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
    33     & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\
    34     & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\
    34     & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
    35     & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
    35     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
    36     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
    36     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
    37     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\