proper spaces around @{text};
authorwenzelm
Wed Oct 21 00:23:11 2015 +0200 (2015-10-21)
changeset 6149463b18f758874
parent 61493 0debd22f0c0e
child 61495 5199b011ecbe
proper spaces around @{text};
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/NEWS	Tue Oct 20 23:53:40 2015 +0200
     1.2 +++ b/NEWS	Wed Oct 21 00:23:11 2015 +0200
     1.3 @@ -73,7 +73,8 @@
     1.4  * The @{text} antiquotation now ignores the antiquotation option
     1.5  "source". The given text content is output unconditionally, without any
     1.6  surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
     1.7 -argument where they are really intended, e.g. @{text \<open>"foo"\<close>}.
     1.8 +argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial
     1.9 +or terminal spaces are ignored.
    1.10  
    1.11  * HTML presentation uses the standard IsabelleText font and Unicode
    1.12  rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Oct 20 23:53:40 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Oct 21 00:23:11 2015 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4      @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
     2.5      @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
     2.6      @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
     2.7 -    @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
     2.8 +    @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     2.9    \end{matharray}
    2.10  
    2.11    The overall content of an Isabelle/Isar theory may alternate between
     3.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Oct 20 23:53:40 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Oct 21 00:23:11 2015 +0200
     3.3 @@ -452,7 +452,7 @@
     3.4    as follows:
     3.5  
     3.6    \begin{center}
     3.7 -  \<open>c :: \<close>@{verbatim \<open>"\<close>}\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>"  (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>" [\<close>}\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
     3.8 +  \<open>c ::\<close>~@{verbatim \<open>"\<close>}\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>"  (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>" [\<close>}\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
     3.9    \end{center}
    3.10  
    3.11    This introduces concrete binder syntax \<open>sy x. b\<close>, where
    3.12 @@ -463,7 +463,7 @@
    3.13  
    3.14    Internally, the binder syntax is expanded to something like this:
    3.15    \begin{center}
    3.16 -  \<open>c_binder :: \<close>@{verbatim \<open>"\<close>}\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>"  ("(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)" [0,\<close>}~\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
    3.17 +  \<open>c_binder ::\<close>~@{verbatim \<open>"\<close>}\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>"  ("(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)" [0,\<close>}~\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
    3.18    \end{center}
    3.19  
    3.20    Here @{syntax (inner) idts} is the nonterminal symbol for a list of
    3.21 @@ -685,29 +685,29 @@
    3.22      & \<open>|\<close> & @{verbatim PROP} \<open>aprop\<close> \\\\
    3.23  
    3.24    @{syntax_def (inner) aprop} & = & @{verbatim "("} \<open>aprop\<close> @{verbatim ")"} \\
    3.25 -    & \<open>|\<close> & \<open>id  |  longid  |  var  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "..."} \\
    3.26 -    & \<open>|\<close> & @{verbatim CONST} \<open>id  |  \<close>@{verbatim CONST} \<open>longid\<close> \\
    3.27 -    & \<open>|\<close> & @{verbatim XCONST} \<open>id  |  \<close>@{verbatim XCONST} \<open>longid\<close> \\
    3.28 +    & \<open>|\<close> & \<open>id  |  longid  |  var  |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
    3.29 +    & \<open>|\<close> & @{verbatim CONST} \<open>id  |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
    3.30 +    & \<open>|\<close> & @{verbatim XCONST} \<open>id  |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
    3.31      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\\\
    3.32  
    3.33    @{syntax_def (inner) logic} & = & @{verbatim "("} \<open>logic\<close> @{verbatim ")"} \\
    3.34      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\
    3.35 -    & \<open>|\<close> & \<open>id  |  longid  |  var  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "..."} \\
    3.36 -    & \<open>|\<close> & @{verbatim CONST} \<open>id  |  \<close>@{verbatim CONST} \<open>longid\<close> \\
    3.37 -    & \<open>|\<close> & @{verbatim XCONST} \<open>id  |  \<close>@{verbatim XCONST} \<open>longid\<close> \\
    3.38 +    & \<open>|\<close> & \<open>id  |  longid  |  var  |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
    3.39 +    & \<open>|\<close> & @{verbatim CONST} \<open>id  |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
    3.40 +    & \<open>|\<close> & @{verbatim XCONST} \<open>id  |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
    3.41      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
    3.42      & \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
    3.43      & \<open>|\<close> & @{verbatim "%"} \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
    3.44      & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
    3.45 -    & \<open>|\<close> & @{verbatim op} @{verbatim "=="}\<open>  |  \<close>@{verbatim op} \<open>\<equiv>\<close>\<open>  |  \<close>@{verbatim op} @{verbatim "&&&"} \\
    3.46 -    & \<open>|\<close> & @{verbatim op} @{verbatim "==>"}\<open>  |  \<close>@{verbatim op} \<open>\<Longrightarrow>\<close> \\
    3.47 +    & \<open>|\<close> & @{verbatim op} @{verbatim "=="}~~\<open>|\<close>~~@{verbatim op} \<open>\<equiv>\<close>~~\<open>|\<close>~~@{verbatim op} @{verbatim "&&&"} \\
    3.48 +    & \<open>|\<close> & @{verbatim op} @{verbatim "==>"}~~\<open>|\<close>~~@{verbatim op} \<open>\<Longrightarrow>\<close> \\
    3.49      & \<open>|\<close> & @{verbatim TYPE} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\\\
    3.50  
    3.51 -  @{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}\<open>  |  id  |  \<close>@{verbatim "_"} \\
    3.52 +  @{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}~~\<open>|  id  |\<close>~~@{verbatim "_"} \\
    3.53      & \<open>|\<close> & \<open>id\<close> @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\
    3.54      & \<open>|\<close> & @{verbatim "_"} @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\\\
    3.55  
    3.56 -  @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}\<open>  |  |  \<index>\<close> \\\\
    3.57 +  @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}~~\<open>|  |  \<index>\<close> \\\\
    3.58  
    3.59    @{syntax_def (inner) idts} & = & \<open>idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts\<close> & \<open>(0)\<close> \\\\
    3.60  
    3.61 @@ -716,8 +716,8 @@
    3.62    @{syntax_def (inner) pttrns} & = & \<open>pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns\<close> & \<open>(0)\<close> \\\\
    3.63  
    3.64    @{syntax_def (inner) type} & = & @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\
    3.65 -    & \<open>|\<close> & \<open>tid  |  tvar  |  \<close>@{verbatim "_"} \\
    3.66 -    & \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort  |  tvar  \<close>@{verbatim "::"} \<open>sort  |  \<close>@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\
    3.67 +    & \<open>|\<close> & \<open>tid  |  tvar  |\<close>~~@{verbatim "_"} \\
    3.68 +    & \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort  |  tvar\<close>~~@{verbatim "::"} \<open>sort  |\<close>~~@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\
    3.69      & \<open>|\<close> & \<open>type_name  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name\<close> \\
    3.70      & \<open>|\<close> & @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim ")"} \<open>type_name\<close> \\
    3.71      & \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\
    3.72 @@ -726,7 +726,7 @@
    3.73      & \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
    3.74    @{syntax_def (inner) type_name} & = & \<open>id  |  longid\<close> \\\\
    3.75  
    3.76 -  @{syntax_def (inner) sort} & = & @{syntax class_name}~\<open>  |  \<close>@{verbatim "{}"} \\
    3.77 +  @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~@{verbatim "{}"} \\
    3.78      & \<open>|\<close> & @{verbatim "{"} @{syntax class_name} @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
    3.79    @{syntax_def (inner) class_name} & = & \<open>id  |  longid\<close> \\
    3.80    \end{supertabular}
    3.81 @@ -1173,7 +1173,7 @@
    3.82    with other syntax declarations.
    3.83  
    3.84    \<^medskip>
    3.85 -  The special case of copy production is specified by \<open>c = \<close>@{verbatim \<open>""\<close>} (empty string).  It means that the
    3.86 +  The special case of copy production is specified by \<open>c =\<close>~@{verbatim \<open>""\<close>} (empty string).  It means that the
    3.87    resulting parse tree \<open>t\<close> is copied directly, without any
    3.88    further decoration.
    3.89  
     4.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Oct 20 23:53:40 2015 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 21 00:23:11 2015 +0200
     4.3 @@ -103,32 +103,32 @@
     4.4    \begin{supertabular}{rcl}
     4.5      @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
     4.6      @{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\
     4.7 -    @{syntax_def symident} & = & \<open>sym\<^sup>+  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
     4.8 +    @{syntax_def symident} & = & \<open>sym\<^sup>+  |\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
     4.9      @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
    4.10 -    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}\<open>  |  \<close>@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
    4.11 -    @{syntax_def var} & = & @{verbatim "?"}\<open>ident  |  \<close>@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
    4.12 +    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}~~\<open>|\<close>~~@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
    4.13 +    @{syntax_def var} & = & @{verbatim "?"}\<open>ident  |\<close>~~@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
    4.14      @{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\
    4.15 -    @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree  |  \<close>@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
    4.16 +    @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree  |\<close>~~@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
    4.17      @{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
    4.18      @{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\
    4.19      @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
    4.20      @{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex]
    4.21  
    4.22 -    \<open>letter\<close> & = & \<open>latin  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}\<open>  |  greek  |\<close> \\
    4.23 +    \<open>letter\<close> & = & \<open>latin  |\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}~~\<open>|\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}~~\<open>|  greek  |\<close> \\
    4.24      \<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\
    4.25 -    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "'"} \\
    4.26 -    \<open>latin\<close> & = & @{verbatim a}\<open>  | \<dots> |  \<close>@{verbatim z}\<open>  |  \<close>@{verbatim A}\<open>  |  \<dots> |  \<close>@{verbatim Z} \\
    4.27 -    \<open>digit\<close> & = & @{verbatim "0"}\<open>  |  \<dots> |  \<close>@{verbatim "9"} \\
    4.28 -    \<open>sym\<close> & = & @{verbatim "!"}\<open>  |  \<close>@{verbatim "#"}\<open>  |  \<close>@{verbatim "$"}\<open>  |  \<close>@{verbatim "%"}\<open>  |  \<close>@{verbatim "&"}\<open>  |  \<close>@{verbatim "*"}\<open>  |  \<close>@{verbatim "+"}\<open>  |  \<close>@{verbatim "-"}\<open>  |  \<close>@{verbatim "/"}\<open>  |\<close> \\
    4.29 -    & & @{verbatim "<"}\<open>  |  \<close>@{verbatim "="}\<open>  |  \<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim "?"}\<open>  |  \<close>@{verbatim "@"}\<open>  |  \<close>@{verbatim "^"}\<open>  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "|"}\<open>  |  \<close>@{verbatim "~"} \\
    4.30 -    \<open>greek\<close> & = & @{verbatim "\<alpha>"}\<open>  |  \<close>@{verbatim "\<beta>"}\<open>  |  \<close>@{verbatim "\<gamma>"}\<open>  |  \<close>@{verbatim "\<delta>"}\<open>  |\<close> \\
    4.31 -          &   & @{verbatim "\<epsilon>"}\<open>  |  \<close>@{verbatim "\<zeta>"}\<open>  |  \<close>@{verbatim "\<eta>"}\<open>  |  \<close>@{verbatim "\<theta>"}\<open>  |\<close> \\
    4.32 -          &   & @{verbatim "\<iota>"}\<open>  |  \<close>@{verbatim "\<kappa>"}\<open>  |  \<close>@{verbatim "\<mu>"}\<open>  |  \<close>@{verbatim "\<nu>"}\<open>  |\<close> \\
    4.33 -          &   & @{verbatim "\<xi>"}\<open>  |  \<close>@{verbatim "\<pi>"}\<open>  |  \<close>@{verbatim "\<rho>"}\<open>  |  \<close>@{verbatim "\<sigma>"}\<open>  |  \<close>@{verbatim "\<tau>"}\<open>  |\<close> \\
    4.34 -          &   & @{verbatim "\<upsilon>"}\<open>  |  \<close>@{verbatim "\<phi>"}\<open>  |  \<close>@{verbatim "\<chi>"}\<open>  |  \<close>@{verbatim "\<psi>"}\<open>  |\<close> \\
    4.35 -          &   & @{verbatim "\<omega>"}\<open>  |  \<close>@{verbatim "\<Gamma>"}\<open>  |  \<close>@{verbatim "\<Delta>"}\<open>  |  \<close>@{verbatim "\<Theta>"}\<open>  |\<close> \\
    4.36 -          &   & @{verbatim "\<Lambda>"}\<open>  |  \<close>@{verbatim "\<Xi>"}\<open>  |  \<close>@{verbatim "\<Pi>"}\<open>  |  \<close>@{verbatim "\<Sigma>"}\<open>  |\<close> \\
    4.37 -          &   & @{verbatim "\<Upsilon>"}\<open>  |  \<close>@{verbatim "\<Phi>"}\<open>  |  \<close>@{verbatim "\<Psi>"}\<open>  |  \<close>@{verbatim "\<Omega>"} \\
    4.38 +    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "'"} \\
    4.39 +    \<open>latin\<close> & = & @{verbatim a}~~\<open>| \<dots> |\<close>~~@{verbatim z}~~\<open>|\<close>~~@{verbatim A}~~\<open>|  \<dots> |\<close>~~@{verbatim Z} \\
    4.40 +    \<open>digit\<close> & = & @{verbatim "0"}~~\<open>|  \<dots> |\<close>~~@{verbatim "9"} \\
    4.41 +    \<open>sym\<close> & = & @{verbatim "!"}~~\<open>|\<close>~~@{verbatim "#"}~~\<open>|\<close>~~@{verbatim "$"}~~\<open>|\<close>~~@{verbatim "%"}~~\<open>|\<close>~~@{verbatim "&"}~~\<open>|\<close>~~@{verbatim "*"}~~\<open>|\<close>~~@{verbatim "+"}~~\<open>|\<close>~~@{verbatim "-"}~~\<open>|\<close>~~@{verbatim "/"}~~\<open>|\<close> \\
    4.42 +    & & @{verbatim "<"}~~\<open>|\<close>~~@{verbatim "="}~~\<open>|\<close>~~@{verbatim ">"}~~\<open>|\<close>~~@{verbatim "?"}~~\<open>|\<close>~~@{verbatim "@"}~~\<open>|\<close>~~@{verbatim "^"}~~\<open>|\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "|"}~~\<open>|\<close>~~@{verbatim "~"} \\
    4.43 +    \<open>greek\<close> & = & @{verbatim "\<alpha>"}~~\<open>|\<close>~~@{verbatim "\<beta>"}~~\<open>|\<close>~~@{verbatim "\<gamma>"}~~\<open>|\<close>~~@{verbatim "\<delta>"}~~\<open>|\<close> \\
    4.44 +          &   & @{verbatim "\<epsilon>"}~~\<open>|\<close>~~@{verbatim "\<zeta>"}~~\<open>|\<close>~~@{verbatim "\<eta>"}~~\<open>|\<close>~~@{verbatim "\<theta>"}~~\<open>|\<close> \\
    4.45 +          &   & @{verbatim "\<iota>"}~~\<open>|\<close>~~@{verbatim "\<kappa>"}~~\<open>|\<close>~~@{verbatim "\<mu>"}~~\<open>|\<close>~~@{verbatim "\<nu>"}~~\<open>|\<close> \\
    4.46 +          &   & @{verbatim "\<xi>"}~~\<open>|\<close>~~@{verbatim "\<pi>"}~~\<open>|\<close>~~@{verbatim "\<rho>"}~~\<open>|\<close>~~@{verbatim "\<sigma>"}~~\<open>|\<close>~~@{verbatim "\<tau>"}~~\<open>|\<close> \\
    4.47 +          &   & @{verbatim "\<upsilon>"}~~\<open>|\<close>~~@{verbatim "\<phi>"}~~\<open>|\<close>~~@{verbatim "\<chi>"}~~\<open>|\<close>~~@{verbatim "\<psi>"}~~\<open>|\<close> \\
    4.48 +          &   & @{verbatim "\<omega>"}~~\<open>|\<close>~~@{verbatim "\<Gamma>"}~~\<open>|\<close>~~@{verbatim "\<Delta>"}~~\<open>|\<close>~~@{verbatim "\<Theta>"}~~\<open>|\<close> \\
    4.49 +          &   & @{verbatim "\<Lambda>"}~~\<open>|\<close>~~@{verbatim "\<Xi>"}~~\<open>|\<close>~~@{verbatim "\<Pi>"}~~\<open>|\<close>~~@{verbatim "\<Sigma>"}~~\<open>|\<close> \\
    4.50 +          &   & @{verbatim "\<Upsilon>"}~~\<open>|\<close>~~@{verbatim "\<Phi>"}~~\<open>|\<close>~~@{verbatim "\<Psi>"}~~\<open>|\<close>~~@{verbatim "\<Omega>"} \\
    4.51    \end{supertabular}
    4.52    \end{center}
    4.53  
     5.1 --- a/src/Doc/Isar_Ref/Proof.thy	Tue Oct 20 23:53:40 2015 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Wed Oct 21 00:23:11 2015 +0200
     5.3 @@ -1398,7 +1398,7 @@
     5.4    \<close>}
     5.5  
     5.6    \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
     5.7 -  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<close> states a rule for case
     5.8 +  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case
     5.9    splitting into separate subgoals, such that each case involves new
    5.10    parameters and premises. After the proof is finished, the resulting rule
    5.11    may be used directly with the @{method cases} proof method
     6.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Oct 20 23:53:40 2015 +0200
     6.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Oct 21 00:23:11 2015 +0200
     6.3 @@ -217,7 +217,7 @@
     6.4  text \<open>
     6.5    \begin{matharray}{rcl}
     6.6      @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     6.7 -    @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
     6.8 +    @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     6.9      @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
    6.10      @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
    6.11      @{keyword_def "includes"} & : & syntax \\
    6.12 @@ -292,9 +292,9 @@
    6.13    \begin{matharray}{rcll}
    6.14      @{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    6.15      @{attribute_def "defn"} & : & \<open>attribute\<close> \\
    6.16 -    @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
    6.17 +    @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    6.18      @{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    6.19 -    @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
    6.20 +    @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    6.21    \end{matharray}
    6.22  
    6.23    Term definitions may either happen within the logic (as equational axioms