doc-src/IsarRef/Thy/Proof.thy

   (three dots).  The canonical application of this convenience are
   calculational proofs (see \secref{sec:calculation}).
 *}
 
 
-subsection {* Facts and forward chaining *}
+subsection {* Facts and forward chaining \label{sec:proof-facts} *}
 
 text {*
   \begin{matharray}{rcl}
     @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
   
     goal: (@{syntax props} + @'and')
     ;
-    longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
+    longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion
     ;
     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
     ;
     case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
   "}

   \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
   @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
   \<phi>"} to be put back into the target context.  An additional @{syntax
   context} specification may build up an initial proof context for the
   subsequent claim; this includes local definitions and syntax as
-  well, see the definition of @{syntax context_elem} in
-  \secref{sec:locale}.
+  well, see also @{syntax "includes"} in \secref{sec:bundle} and
+  @{syntax context_elem} in \secref{sec:locale}.
   
   \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
   "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
   "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
   being of a different kind.  This discrimination acts like a formal