src/Doc/Isar_Ref/Proof.thy
changeset 60130 8044de95819b
parent 59992 d8db5172c23f
child 60131 2506f17d2739
equal deleted inserted replaced
60128:3d696ccb7fa6 60130:8044de95819b
   442     goal: (@{syntax props} + @'and')
   442     goal: (@{syntax props} + @'and')
   443     ;
   443     ;
   444     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
   444     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
   445       conclusion
   445       conclusion
   446     ;
   446     ;
   447     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
   447     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? obtain_case + '|')
   448     ;
   448     ;
   449     case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
   449     obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   450   \<close>}
   450   \<close>}
   451 
   451 
   452   \begin{description}
   452   \begin{description}
   453   
   453   
   454   \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
   454   \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with