--- a/NEWS Tue Oct 20 23:53:40 2015 +0200
+++ b/NEWS Wed Oct 21 00:23:11 2015 +0200
@@ -73,7 +73,8 @@
* The @{text} antiquotation now ignores the antiquotation option
"source". The given text content is output unconditionally, without any
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
-argument where they are really intended, e.g. @{text \<open>"foo"\<close>}.
+argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial
+or terminal spaces are ignored.
* HTML presentation uses the standard IsabelleText font and Unicode
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue Oct 20 23:53:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed Oct 21 00:23:11 2015 +0200
@@ -109,7 +109,7 @@
@{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
- @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
+ @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
The overall content of an Isabelle/Isar theory may alternate between
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 20 23:53:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Oct 21 00:23:11 2015 +0200
@@ -452,7 +452,7 @@
as follows:
\begin{center}
- \<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 ")"}
+ \<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 ")"}
\end{center}
This introduces concrete binder syntax \<open>sy x. b\<close>, where
@@ -463,7 +463,7 @@
Internally, the binder syntax is expanded to something like this:
\begin{center}
- \<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 ")"}
+ \<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 ")"}
\end{center}
Here @{syntax (inner) idts} is the nonterminal symbol for a list of
@@ -685,29 +685,29 @@
& \<open>|\<close> & @{verbatim PROP} \<open>aprop\<close> \\\\
@{syntax_def (inner) aprop} & = & @{verbatim "("} \<open>aprop\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>id | longid | var | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "..."} \\
- & \<open>|\<close> & @{verbatim CONST} \<open>id | \<close>@{verbatim CONST} \<open>longid\<close> \\
- & \<open>|\<close> & @{verbatim XCONST} \<open>id | \<close>@{verbatim XCONST} \<open>longid\<close> \\
+ & \<open>|\<close> & \<open>id | longid | var |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
+ & \<open>|\<close> & @{verbatim CONST} \<open>id |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
+ & \<open>|\<close> & @{verbatim XCONST} \<open>id |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
& \<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> \\\\
@{syntax_def (inner) logic} & = & @{verbatim "("} \<open>logic\<close> @{verbatim ")"} \\
& \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & \<open>id | longid | var | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "..."} \\
- & \<open>|\<close> & @{verbatim CONST} \<open>id | \<close>@{verbatim CONST} \<open>longid\<close> \\
- & \<open>|\<close> & @{verbatim XCONST} \<open>id | \<close>@{verbatim XCONST} \<open>longid\<close> \\
+ & \<open>|\<close> & \<open>id | longid | var |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
+ & \<open>|\<close> & @{verbatim CONST} \<open>id |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
+ & \<open>|\<close> & @{verbatim XCONST} \<open>id |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
& \<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> \\
& \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
& \<open>|\<close> & @{verbatim "%"} \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
& \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & @{verbatim op} @{verbatim "=="}\<open> | \<close>@{verbatim op} \<open>\<equiv>\<close>\<open> | \<close>@{verbatim op} @{verbatim "&&&"} \\
- & \<open>|\<close> & @{verbatim op} @{verbatim "==>"}\<open> | \<close>@{verbatim op} \<open>\<Longrightarrow>\<close> \\
+ & \<open>|\<close> & @{verbatim op} @{verbatim "=="}~~\<open>|\<close>~~@{verbatim op} \<open>\<equiv>\<close>~~\<open>|\<close>~~@{verbatim op} @{verbatim "&&&"} \\
+ & \<open>|\<close> & @{verbatim op} @{verbatim "==>"}~~\<open>|\<close>~~@{verbatim op} \<open>\<Longrightarrow>\<close> \\
& \<open>|\<close> & @{verbatim TYPE} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\\\
- @{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}\<open> | id | \<close>@{verbatim "_"} \\
+ @{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}~~\<open>| id |\<close>~~@{verbatim "_"} \\
& \<open>|\<close> & \<open>id\<close> @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\
& \<open>|\<close> & @{verbatim "_"} @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\\\
- @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}\<open> | | \<index>\<close> \\\\
+ @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}~~\<open>| | \<index>\<close> \\\\
@{syntax_def (inner) idts} & = & \<open>idt | idt\<^sup>(\<^sup>1\<^sup>) idts\<close> & \<open>(0)\<close> \\\\
@@ -716,8 +716,8 @@
@{syntax_def (inner) pttrns} & = & \<open>pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns\<close> & \<open>(0)\<close> \\\\
@{syntax_def (inner) type} & = & @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>tid | tvar | \<close>@{verbatim "_"} \\
- & \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort | tvar \<close>@{verbatim "::"} \<open>sort | \<close>@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\
+ & \<open>|\<close> & \<open>tid | tvar |\<close>~~@{verbatim "_"} \\
+ & \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort | tvar\<close>~~@{verbatim "::"} \<open>sort |\<close>~~@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\
& \<open>|\<close> & \<open>type_name | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name\<close> \\
& \<open>|\<close> & @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim ")"} \<open>type_name\<close> \\
& \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\
@@ -726,7 +726,7 @@
& \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
@{syntax_def (inner) type_name} & = & \<open>id | longid\<close> \\\\
- @{syntax_def (inner) sort} & = & @{syntax class_name}~\<open> | \<close>@{verbatim "{}"} \\
+ @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~@{verbatim "{}"} \\
& \<open>|\<close> & @{verbatim "{"} @{syntax class_name} @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
@{syntax_def (inner) class_name} & = & \<open>id | longid\<close> \\
\end{supertabular}
@@ -1173,7 +1173,7 @@
with other syntax declarations.
\<^medskip>
- The special case of copy production is specified by \<open>c = \<close>@{verbatim \<open>""\<close>} (empty string). It means that the
+ The special case of copy production is specified by \<open>c =\<close>~@{verbatim \<open>""\<close>} (empty string). It means that the
resulting parse tree \<open>t\<close> is copied directly, without any
further decoration.
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Tue Oct 20 23:53:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Wed Oct 21 00:23:11 2015 +0200
@@ -103,32 +103,32 @@
\begin{supertabular}{rcl}
@{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
@{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\
- @{syntax_def symident} & = & \<open>sym\<^sup>+ | \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
+ @{syntax_def symident} & = & \<open>sym\<^sup>+ |\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
@{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
- @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}\<open> | \<close>@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
- @{syntax_def var} & = & @{verbatim "?"}\<open>ident | \<close>@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
+ @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}~~\<open>|\<close>~~@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
+ @{syntax_def var} & = & @{verbatim "?"}\<open>ident |\<close>~~@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
@{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\
- @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree | \<close>@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
+ @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree |\<close>~~@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
@{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
@{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\
@{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
@{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex]
- \<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> \\
+ \<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> \\
\<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\
- \<open>quasiletter\<close> & = & \<open>letter | digit | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "'"} \\
- \<open>latin\<close> & = & @{verbatim a}\<open> | \<dots> | \<close>@{verbatim z}\<open> | \<close>@{verbatim A}\<open> | \<dots> | \<close>@{verbatim Z} \\
- \<open>digit\<close> & = & @{verbatim "0"}\<open> | \<dots> | \<close>@{verbatim "9"} \\
- \<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> \\
- & & @{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>greek\<close> & = & @{verbatim "\<alpha>"}\<open> | \<close>@{verbatim "\<beta>"}\<open> | \<close>@{verbatim "\<gamma>"}\<open> | \<close>@{verbatim "\<delta>"}\<open> |\<close> \\
- & & @{verbatim "\<epsilon>"}\<open> | \<close>@{verbatim "\<zeta>"}\<open> | \<close>@{verbatim "\<eta>"}\<open> | \<close>@{verbatim "\<theta>"}\<open> |\<close> \\
- & & @{verbatim "\<iota>"}\<open> | \<close>@{verbatim "\<kappa>"}\<open> | \<close>@{verbatim "\<mu>"}\<open> | \<close>@{verbatim "\<nu>"}\<open> |\<close> \\
- & & @{verbatim "\<xi>"}\<open> | \<close>@{verbatim "\<pi>"}\<open> | \<close>@{verbatim "\<rho>"}\<open> | \<close>@{verbatim "\<sigma>"}\<open> | \<close>@{verbatim "\<tau>"}\<open> |\<close> \\
- & & @{verbatim "\<upsilon>"}\<open> | \<close>@{verbatim "\<phi>"}\<open> | \<close>@{verbatim "\<chi>"}\<open> | \<close>@{verbatim "\<psi>"}\<open> |\<close> \\
- & & @{verbatim "\<omega>"}\<open> | \<close>@{verbatim "\<Gamma>"}\<open> | \<close>@{verbatim "\<Delta>"}\<open> | \<close>@{verbatim "\<Theta>"}\<open> |\<close> \\
- & & @{verbatim "\<Lambda>"}\<open> | \<close>@{verbatim "\<Xi>"}\<open> | \<close>@{verbatim "\<Pi>"}\<open> | \<close>@{verbatim "\<Sigma>"}\<open> |\<close> \\
- & & @{verbatim "\<Upsilon>"}\<open> | \<close>@{verbatim "\<Phi>"}\<open> | \<close>@{verbatim "\<Psi>"}\<open> | \<close>@{verbatim "\<Omega>"} \\
+ \<open>quasiletter\<close> & = & \<open>letter | digit |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "'"} \\
+ \<open>latin\<close> & = & @{verbatim a}~~\<open>| \<dots> |\<close>~~@{verbatim z}~~\<open>|\<close>~~@{verbatim A}~~\<open>| \<dots> |\<close>~~@{verbatim Z} \\
+ \<open>digit\<close> & = & @{verbatim "0"}~~\<open>| \<dots> |\<close>~~@{verbatim "9"} \\
+ \<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> \\
+ & & @{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>greek\<close> & = & @{verbatim "\<alpha>"}~~\<open>|\<close>~~@{verbatim "\<beta>"}~~\<open>|\<close>~~@{verbatim "\<gamma>"}~~\<open>|\<close>~~@{verbatim "\<delta>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<epsilon>"}~~\<open>|\<close>~~@{verbatim "\<zeta>"}~~\<open>|\<close>~~@{verbatim "\<eta>"}~~\<open>|\<close>~~@{verbatim "\<theta>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<iota>"}~~\<open>|\<close>~~@{verbatim "\<kappa>"}~~\<open>|\<close>~~@{verbatim "\<mu>"}~~\<open>|\<close>~~@{verbatim "\<nu>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<xi>"}~~\<open>|\<close>~~@{verbatim "\<pi>"}~~\<open>|\<close>~~@{verbatim "\<rho>"}~~\<open>|\<close>~~@{verbatim "\<sigma>"}~~\<open>|\<close>~~@{verbatim "\<tau>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<upsilon>"}~~\<open>|\<close>~~@{verbatim "\<phi>"}~~\<open>|\<close>~~@{verbatim "\<chi>"}~~\<open>|\<close>~~@{verbatim "\<psi>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<omega>"}~~\<open>|\<close>~~@{verbatim "\<Gamma>"}~~\<open>|\<close>~~@{verbatim "\<Delta>"}~~\<open>|\<close>~~@{verbatim "\<Theta>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<Lambda>"}~~\<open>|\<close>~~@{verbatim "\<Xi>"}~~\<open>|\<close>~~@{verbatim "\<Pi>"}~~\<open>|\<close>~~@{verbatim "\<Sigma>"}~~\<open>|\<close> \\
+ & & @{verbatim "\<Upsilon>"}~~\<open>|\<close>~~@{verbatim "\<Phi>"}~~\<open>|\<close>~~@{verbatim "\<Psi>"}~~\<open>|\<close>~~@{verbatim "\<Omega>"} \\
\end{supertabular}
\end{center}
--- a/src/Doc/Isar_Ref/Proof.thy Tue Oct 20 23:53:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Oct 21 00:23:11 2015 +0200
@@ -1398,7 +1398,7 @@
\<close>}
\<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
- | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<close> states a rule for case
+ | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case
splitting into separate subgoals, such that each case involves new
parameters and premises. After the proof is finished, the resulting rule
may be used directly with the @{method cases} proof method
--- a/src/Doc/Isar_Ref/Spec.thy Tue Oct 20 23:53:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Oct 21 00:23:11 2015 +0200
@@ -217,7 +217,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
- @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
+ @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@{keyword_def "includes"} & : & syntax \\
@@ -292,9 +292,9 @@
\begin{matharray}{rcll}
@{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{attribute_def "defn"} & : & \<open>attribute\<close> \\
- @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
+ @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
- @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \<close> \\
+ @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
Term definitions may either happen within the logic (as equational axioms