--- a/NEWS Tue May 03 21:46:49 2011 +0200
+++ b/NEWS Tue May 03 22:28:19 2011 +0200
@@ -37,12 +37,16 @@
Note that automated detection from the file-system or search path has
been discontinued. INCOMPATIBILITY.
-* Name space: proper configuration options "long_names",
-"short_names", "unique_names" instead of former unsynchronized
-references. Minor INCOMPATIBILITY, need to declare options in context
-like this:
-
- declare [[unique_names = false]]
+* Name space: former unsynchronized references are now proper
+configuration options, with more conventional names:
+
+ long_names ~> names_long
+ short_names ~> names_short
+ unique_names ~> names_unique
+
+Minor INCOMPATIBILITY, need to declare options in context like this:
+
+ declare [[names_unique = false]]
* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note
that the result needs to be unique, which means fact specifications
--- a/doc-src/Codegen/Thy/Setup.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Tue May 03 22:28:19 2011 +0200
@@ -22,6 +22,6 @@
setup {* Code_Target.set_default_code_width 74 *}
-declare [[unique_names = false]]
+declare [[names_unique = false]]
end
--- a/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 22:28:19 2011 +0200
@@ -517,14 +517,14 @@
\infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
\]
\[
- \infer[@{text "(\<And>\<dash>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
+ \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
\qquad
- \infer[@{text "(\<And>\<dash>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
+ \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
\]
\[
- \infer[@{text "(\<Longrightarrow>\<dash>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\qquad
- \infer[@{text "(\<Longrightarrow>\<dash>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
+ \infer[@{text "(\<Longrightarrow>\<hyphen>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
@@ -554,7 +554,7 @@
\cite{Berghofer-Nipkow:2000:TPHOL}).
Observe that locally fixed parameters (as in @{text
- "\<And>\<dash>intro"}) need not be recorded in the hypotheses, because
+ "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
the simple syntactic types of Pure are always inhabitable.
``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement
--- a/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 22:28:19 2011 +0200
@@ -667,7 +667,7 @@
ML is augmented by special syntactic entities of the following form:
@{rail "
- @{syntax_def antiquote}: '@' '{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
+ @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
"}
Here @{syntax nameref} and @{syntax args} are regular outer syntax
--- a/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 22:28:19 2011 +0200
@@ -253,14 +253,14 @@
\medskip The most basic export rule discharges assumptions directly
by means of the @{text "\<Longrightarrow>"} introduction rule:
\[
- \infer[(@{text "\<Longrightarrow>\<dash>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\]
The variant for goal refinements marks the newly introduced
premises, which causes the canonical Isar goal refinement scheme to
enforce unification with local premises within the goal:
\[
- \infer[(@{text "#\<Longrightarrow>\<dash>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\]
\medskip Alternative versions of assumptions may perform arbitrary
@@ -269,7 +269,7 @@
definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
with the following export rule to reverse the effect:
\[
- \infer[(@{text "\<equiv>\<dash>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
+ \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
\]
This works, because the assumption @{text "x \<equiv> t"} was introduced in
a context with @{text "x"} being fresh, so @{text "x"} does not
@@ -307,7 +307,7 @@
\item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
@{ML Assumption.add_assms} where the export rule performs @{text
- "\<Longrightarrow>\<dash>intro"} or @{text "#\<Longrightarrow>\<dash>intro"}, depending on goal
+ "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal
mode.
\item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 22:28:19 2011 +0200
@@ -217,15 +217,15 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[]
\rail@nont{\isa{nameref}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]
\rail@nont{\isa{sort}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
\rail@nextbar{1}
@@ -235,7 +235,7 @@
\rail@endbar
\rail@nont{\isa{nameref}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]
\rail@nont{\isa{type}}[]
\rail@end
@@ -481,7 +481,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
\rail@nextbar{1}
@@ -489,7 +489,7 @@
\rail@endbar
\rail@nont{\isa{nameref}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -502,11 +502,11 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]
\rail@nont{\isa{term}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]
\rail@nont{\isa{prop}}[]
\rail@end
@@ -592,14 +592,14 @@
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{}
\]
\[
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}
\qquad
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}
\]
\[
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\qquad
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
@@ -626,7 +626,7 @@
terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\
\cite{Berghofer-Nipkow:2000:TPHOL}).
- Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}) need not be recorded in the hypotheses, because
+ Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}) need not be recorded in the hypotheses, because
the simple syntactic types of Pure are always inhabitable.
``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only
present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement
@@ -813,27 +813,27 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]
\rail@nont{\isa{typ}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]
\rail@nont{\isa{term}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]
\rail@nont{\isa{prop}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]
\rail@nont{\isa{thmref}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]
\rail@nont{\isa{thmrefs}}[]
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]
\rail@bar
\rail@nextbar{1}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 22:28:19 2011 +0200
@@ -799,8 +799,7 @@
\begin{railoutput}
\rail@begin{3}{\indexdef{}{syntax}{antiquote}\hypertarget{syntax.antiquote}{\hyperlink{syntax.antiquote}{\mbox{\isa{antiquote}}}}}
\rail@bar
-\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[]
-\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
+\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
\rail@nont{\isa{nameref}}[]
\rail@nont{\isa{args}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
@@ -849,7 +848,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[]
\rail@plus
\rail@plus
@@ -863,7 +862,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[]
\rail@plus
\rail@bar
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 03 22:28:19 2011 +0200
@@ -265,7 +265,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1721,7 +1721,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[]
\rail@nont{\isa{name}}[]
\rail@end
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 22:28:19 2011 +0200
@@ -397,14 +397,14 @@
\medskip The most basic export rule discharges assumptions directly
by means of the \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction rule:
\[
- \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\]
The variant for goal refinements marks the newly introduced
premises, which causes the canonical Isar goal refinement scheme to
enforce unification with local premises within the goal:
\[
- \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\]
\medskip Alternative versions of assumptions may perform arbitrary
@@ -413,7 +413,7 @@
definition works by fixing \isa{x} and assuming \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t},
with the following export rule to reverse the effect:
\[
- \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C646173683E}{\isasymdash}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}}
+ \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}}
\]
This works, because the assumption \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} was introduced in
a context with \isa{x} being fresh, so \isa{x} does not
@@ -455,7 +455,7 @@
\verb|Assumption.assume|.
\item \verb|Assumption.add_assumes|~\isa{As} is a special case of
- \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}, depending on goal
+ \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}, depending on goal
mode.
\item \verb|Assumption.export|~\isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ inner\ outer\ thm}
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Tue May 03 22:28:19 2011 +0200
@@ -168,7 +168,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarImplementation/style.sty Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarImplementation/style.sty Tue May 03 22:28:19 2011 +0200
@@ -64,15 +64,8 @@
\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-\isabellestyle{it}
-\newcommand{\isasymdash}{\mbox{-}}
+\isabellestyle{itunderscore}
-\underscoreon
-\newcommand{\setupunderscore}{\def\isacharunderscore{\_}\def\isacharunderscorekeyword{\_}}
-\setupunderscore
-
-\makeatletter
-\def\rail@termfont{\isabellestyle{tt}\setupunderscore}
-\def\rail@nontfont{\isabellestyle{it}\setupunderscore}
-\def\rail@namefont{\isabellestyle{it}\setupunderscore}
-\makeatother
+\railtermfont{\isabellestyle{tt}}
+\railnontermfont{\isabellestyle{itunderscore}}
+\railnamefont{\isabellestyle{itunderscore}}
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue May 03 22:28:19 2011 +0200
@@ -341,16 +341,16 @@
\item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
controls folding of abbreviations.
- \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
+ \item @{antiquotation_option_def names_long}~@{text "= bool"} forces
names of types and constants etc.\ to be printed in their fully
qualified internal form.
- \item @{antiquotation_option_def short_names}~@{text "= bool"}
+ \item @{antiquotation_option_def names_short}~@{text "= bool"}
forces names of types and constants etc.\ to be printed unqualified.
Note that internalizing the output again in the current context may
well yield a different result.
- \item @{antiquotation_option_def unique_names}~@{text "= bool"}
+ \item @{antiquotation_option_def names_unique}~@{text "= bool"}
determines whether the printed version of qualified names should be
made sufficiently long to avoid overlap with names declared further
back. Set to @{text false} for more concise output.
--- a/doc-src/IsarRef/Thy/Framework.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy Tue May 03 22:28:19 2011 +0200
@@ -424,7 +424,7 @@
\infer[(@{inference refinement})]
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
{\begin{tabular}{rl}
- @{text "sub\<dash>proof:"} &
+ @{text "sub\<hyphen>proof:"} &
@{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
@{text "goal:"} &
@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
@@ -436,7 +436,7 @@
\end{tabular}}
\]
- \noindent Here the @{text "sub\<dash>proof"} rule stems from the
+ \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
main @{command fix}-@{command assume}-@{command show} outline of
Isar (cf.\ \secref{sec:framework-subproof}): each assumption
indicated in the text results in a marked premise @{text "G"} above.
@@ -466,7 +466,7 @@
\medskip
\begin{tabular}{rcl}
- @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
+ @{text "theory\<hyphen>stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
@{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex]
@@ -582,7 +582,7 @@
\medskip
\begin{tabular}{rcl}
- @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<dash>discharge\<guillemotright> A"} \\
+ @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A"} \\
@{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\
\end{tabular}
\medskip
@@ -591,14 +591,14 @@
\infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
\]
\[
- \infer[(@{inference_def "weak\<dash>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
+ \infer[(@{inference_def "weak\<hyphen>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
\]
\[
\infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}}
\]
\medskip Note that @{inference discharge} and @{inference
- "weak\<dash>discharge"} differ in the marker for @{prop A}, which is
+ "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
relevant when the result of a @{command fix}-@{command
assume}-@{command show} outline is composed with a pending goal,
cf.\ \secref{sec:framework-subproof}.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 22:28:19 2011 +0200
@@ -100,9 +100,9 @@
@{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
@{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
@{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
- @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
- @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
- @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
+ @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
@{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
@{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
@{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
@@ -144,8 +144,8 @@
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item @{attribute long_names}, @{attribute short_names}, and
- @{attribute unique_names} control the way of printing fully
+ \item @{attribute names_long}, @{attribute names_short}, and
+ @{attribute names_unique} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
--- a/doc-src/IsarRef/Thy/Quick_Reference.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Tue May 03 22:28:19 2011 +0200
@@ -29,7 +29,7 @@
\begin{tabular}{rcl}
@{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\
- & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[0.5ex]
+ & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\
@{text prfx} & = & @{command "apply"}~@{text method} \\
& @{text "|"} & @{command "using"}~@{text "facts"} \\
& @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
@@ -58,7 +58,7 @@
@{command "hence"} & @{text "\<equiv>"} & @{command "then"}~@{command "have"} \\
@{command "thus"} & @{text "\<equiv>"} & @{command "then"}~@{command "show"} \\
@{command "from"}~@{text a} & @{text "\<equiv>"} & @{command "note"}~@{text a}~@{command "then"} \\
- @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\[0.5ex]
+ @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\
@{command "from"}~@{text this} & @{text "\<equiv>"} & @{command "then"} \\
@{command "from"}~@{text this}~@{command "have"} & @{text "\<equiv>"} & @{command "hence"} \\
@{command "from"}~@{text this}~@{command "show"} & @{text "\<equiv>"} & @{command "thus"} \\
@@ -141,7 +141,7 @@
text {*
\begin{tabular}{ll}
- \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
+ \multicolumn{2}{l}{\textbf{Rules}} \\[0.5ex]
@{attribute OF}~@{text a} & rule resolved with facts (skipping ``@{text _}'') \\
@{attribute of}~@{text t} & rule instantiated with terms (skipping ``@{text _}'') \\
@{attribute "where"}~@{text "x = t"} & rule instantiated with terms, by variable name \\
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue May 03 22:28:19 2011 +0200
@@ -103,7 +103,7 @@
syntax.
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}}[]
\rail@nextbar{1}
@@ -121,7 +121,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@bar
\rail@term{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}}[]
\rail@nextbar{1}
@@ -230,7 +230,7 @@
context.
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
\rail@nont{\isa{antiquotation}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
@@ -497,16 +497,16 @@
\item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
controls folding of abbreviations.
- \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces
+ \item \indexdef{}{antiquotation option}{names\_long}\hypertarget{antiquotation option.names-long}{\hyperlink{antiquotation option.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces
names of types and constants etc.\ to be printed in their fully
qualified internal form.
- \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
+ \item \indexdef{}{antiquotation option}{names\_short}\hypertarget{antiquotation option.names-short}{\hyperlink{antiquotation option.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
forces names of types and constants etc.\ to be printed unqualified.
Note that internalizing the output again in the current context may
well yield a different result.
- \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
+ \item \indexdef{}{antiquotation option}{names\_unique}\hypertarget{antiquotation option.names-unique}{\hyperlink{antiquotation option.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
determines whether the printed version of qualified names should be
made sufficiently long to avoid overlap with names declared further
back. Set to \isa{false} for more concise output.
@@ -642,7 +642,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\isa{rail}}[]
\rail@nont{\isa{string}}[]
\rail@end
@@ -658,7 +658,7 @@
The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@plus
\rail@bar
\rail@nextbar{1}
@@ -750,7 +750,7 @@
\item Empty \verb|()|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@end
\end{railoutput}
@@ -758,7 +758,7 @@
\item Nonterminal \verb|A|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@nont{\isa{A}}[]
\rail@end
\end{railoutput}
@@ -768,7 +768,7 @@
\verb|@{syntax method}|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
\rail@end
\end{railoutput}
@@ -777,7 +777,7 @@
\item Terminal \verb|'xyz'|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\isa{xyz}}[]
\rail@end
\end{railoutput}
@@ -786,7 +786,7 @@
\item Terminal in keyword style \verb|@'xyz'|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\isa{\isakeyword{xyz}}}[]
\rail@end
\end{railoutput}
@@ -796,7 +796,7 @@
\verb|@@{method rule}|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
\rail@end
\end{railoutput}
@@ -805,7 +805,7 @@
\item Concatenation \verb|A B C|
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@nont{\isa{A}}[]
\rail@nont{\isa{B}}[]
\rail@nont{\isa{C}}[]
@@ -819,7 +819,7 @@
second one for escaping.} \verb|A B C \\ D E F|
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@nont{\isa{A}}[]
\rail@nont{\isa{B}}[]
\rail@nont{\isa{C}}[]
@@ -834,7 +834,7 @@
\item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@nont{\isa{A}}[]
\rail@nextbar{1}
@@ -849,7 +849,7 @@
\item Option \verb|A ?|
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{A}}[]
@@ -861,7 +861,7 @@
\item Repetition \verb|A *|
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@plus
\rail@nextplus{1}
\rail@cnont{\isa{A}}[]
@@ -873,7 +873,7 @@
\item Repetition with separator \verb|A * sep|
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@nextbar{1}
\rail@plus
@@ -889,7 +889,7 @@
\item Strict repetition \verb|A +|
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@plus
\rail@nont{\isa{A}}[]
\rail@nextplus{1}
@@ -901,7 +901,7 @@
\item Strict repetition with separator \verb|A + sep|
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@plus
\rail@nont{\isa{A}}[]
\rail@nextplus{1}
@@ -926,7 +926,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isaliteral{5F}{\isacharunderscore}}drafts}}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 22:28:19 2011 +0200
@@ -538,7 +538,7 @@
\infer[(\hyperlink{inference.refinement}{\mbox{\isa{refinement}}})]
{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec G{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{22}{\isachardoublequote}}}}
{\begin{tabular}{rl}
- \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
+ \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec G\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a{\isaliteral{22}{\isachardoublequote}}} \\
\isa{{\isaliteral{22}{\isachardoublequote}}goal{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} \\
@@ -550,7 +550,7 @@
\end{tabular}}
\]
- \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the
+ \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the
main \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline of
Isar (cf.\ \secref{sec:framework-subproof}): each assumption
indicated in the text results in a marked premise \isa{{\isaliteral{22}{\isachardoublequote}}G{\isaliteral{22}{\isachardoublequote}}} above.
@@ -580,7 +580,7 @@
\medskip
\begin{tabular}{rcl}
- \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C646173683E}{\isasymdash}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
+ \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
@@ -687,7 +687,7 @@
\medskip
\begin{tabular}{rcl}
- \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\
+ \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\
\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}expansion{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} \\
\end{tabular}
\medskip
@@ -696,13 +696,13 @@
\infer[(\indexdef{}{inference}{discharge}\hypertarget{inference.discharge}{\hyperlink{inference.discharge}{\mbox{\isa{discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
\]
\[
- \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
+ \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
\]
\[
\infer[(\indexdef{}{inference}{expansion}\hypertarget{inference.expansion}{\hyperlink{inference.expansion}{\mbox{\isa{expansion}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ a{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x{\isaliteral{22}{\isachardoublequote}}}}
\]
- \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}} differ in the marker for \isa{A}, which is
+ \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}} differ in the marker for \isa{A}, which is
relevant when the result of a \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline is composed with a pending goal,
cf.\ \secref{sec:framework-subproof}.
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 22:28:19 2011 +0200
@@ -72,7 +72,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -128,7 +128,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{method.fold}{\mbox{\isa{fold}}}}[]
\rail@nextbar{1}
@@ -138,7 +138,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{method.erule}{\mbox{\isa{erule}}}}[]
\rail@nextbar{1}
@@ -206,16 +206,16 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
\rail@nextbar{1}
@@ -229,7 +229,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}}[]
\rail@nextbar{1}
@@ -237,7 +237,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -297,7 +297,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.subst}{\mbox{\isa{subst}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -316,7 +316,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -426,7 +426,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@nextbar{1}
@@ -452,7 +452,7 @@
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -463,7 +463,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -474,7 +474,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -485,7 +485,7 @@
\rail@nont{\hyperlink{syntax.int}{\mbox{\isa{int}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}[]
\rail@nextbar{1}
@@ -570,7 +570,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{method.simp}{\mbox{\isa{simp}}}}[]
\rail@nextbar{1}
@@ -693,7 +693,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
\rail@nextbar{1}
@@ -738,7 +738,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
@@ -760,7 +760,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.simproc}{\mbox{\isa{simproc}}}}[]
\rail@bar
\rail@bar
@@ -818,7 +818,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -877,7 +877,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
\rail@nextbar{1}
@@ -936,7 +936,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.blast}{\mbox{\isa{blast}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -947,7 +947,7 @@
\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
\rail@endplus
\rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
\rail@nextbar{1}
@@ -1022,7 +1022,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1034,7 +1034,7 @@
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
\rail@endplus
\rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
\rail@nextbar{1}
@@ -1146,7 +1146,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
\rail@nextbar{1}
@@ -1165,11 +1165,11 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
\rail@term{\isa{del}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
\rail@bar
\rail@bar
@@ -1272,11 +1272,11 @@
declarations internally.
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1285,7 +1285,7 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
\rail@bar
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue May 03 22:28:19 2011 +0200
@@ -55,7 +55,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}}[]
\rail@bar
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue May 03 22:28:19 2011 +0200
@@ -32,7 +32,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -123,7 +123,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -237,7 +237,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -410,7 +410,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
\rail@plus
\rail@nont{\isa{dtspec}}[]
@@ -418,7 +418,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -499,7 +499,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -552,7 +552,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -562,7 +562,7 @@
\rail@term{\isa{\isakeyword{where}}}[]
\rail@nont{\isa{equations}}[]
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
\rail@nextbar{1}
@@ -605,7 +605,7 @@
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -696,18 +696,18 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
\rail@plus
\rail@nextplus{1}
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
\rail@nont{\isa{orders}}[]
\rail@plus
@@ -781,7 +781,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -866,7 +866,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -886,7 +886,7 @@
\rail@nont{\isa{hints}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@nont{\isa{recdeftc}}[]
\rail@bar
\rail@nextbar{1}
@@ -968,7 +968,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
\rail@nextbar{1}
@@ -1023,7 +1023,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
\rail@nextbar{1}
@@ -1066,7 +1066,7 @@
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1210,7 +1210,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
\rail@plus
\rail@nextplus{1}
@@ -1246,7 +1246,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1281,7 +1281,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1305,7 +1305,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1322,7 +1322,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1407,7 +1407,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1421,7 +1421,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
\rail@nextbar{1}
@@ -1440,7 +1440,7 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
\rail@nextbar{1}
@@ -1599,7 +1599,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1611,7 +1611,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1630,7 +1630,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
@@ -1645,7 +1645,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
\rail@plus
\rail@bar
@@ -1751,7 +1751,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{constexpr}}[]
@@ -1817,7 +1817,7 @@
\rail@term{\isa{Scala}}[]
\rail@endbar
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1830,35 +1830,35 @@
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{del}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{del}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1868,7 +1868,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1878,7 +1878,7 @@
\rail@endplus
\rail@endbar
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
\rail@plus
\rail@nont{\isa{const}}[]
@@ -1901,7 +1901,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@plus
\rail@nont{\isa{typeconstructor}}[]
@@ -1924,7 +1924,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{9}{\isa{}}
+\rail@begin{9}{}
\rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
\rail@plus
\rail@nont{\isa{class}}[]
@@ -1948,7 +1948,7 @@
\rail@nextplus{8}
\rail@endplus
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
\rail@plus
\rail@nont{\isa{typeconstructor}}[]
@@ -1973,7 +1973,7 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
\rail@nont{\isa{target}}[]
\rail@plus
@@ -1981,13 +1981,13 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
\rail@nont{\isa{const}}[]
\rail@nont{\isa{const}}[]
\rail@nont{\isa{target}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
\rail@nont{\isa{target}}[]
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
@@ -1997,7 +1997,7 @@
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
\rail@nont{\isa{target}}[]
\rail@plus
@@ -2006,7 +2006,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@cr{2}
@@ -2189,7 +2189,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{11}{\isa{}}
+\rail@begin{11}{}
\rail@bar
\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
\rail@nextbar{1}
@@ -2241,7 +2241,7 @@
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{codespec}}[]
@@ -2256,7 +2256,7 @@
\rail@nont{\isa{attachment}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
\rail@plus
\rail@nont{\isa{tycodespec}}[]
@@ -2289,7 +2289,7 @@
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -2565,7 +2565,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 22:28:19 2011 +0200
@@ -45,7 +45,7 @@
internal logical entities in a human-readable fashion.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -53,7 +53,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -61,7 +61,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -69,7 +69,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -77,7 +77,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[]
\rail@nextbar{1}
@@ -92,7 +92,7 @@
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -175,9 +175,9 @@
\indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
\indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
- \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
+ \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
\indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
\indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\
@@ -219,8 +219,8 @@
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
- \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
+ \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and
+ \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
@@ -488,7 +488,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
\rail@nextbar{1}
@@ -510,7 +510,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[]
\rail@nextbar{1}
@@ -532,7 +532,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -899,7 +899,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -907,7 +907,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[]
\rail@nextbar{1}
@@ -922,7 +922,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{7}{\isa{}}
+\rail@begin{7}{}
\rail@bar
\rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[]
\rail@nextbar{1}
@@ -1017,7 +1017,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@bar
\rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Tue May 03 22:28:19 2011 +0200
@@ -42,7 +42,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]
\rail@nextbar{1}
@@ -53,7 +53,7 @@
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
\rail@endbar
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -99,7 +99,7 @@
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]
\rail@plus
\rail@nextplus{1}
@@ -123,11 +123,11 @@
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -259,7 +259,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue May 03 22:28:19 2011 +0200
@@ -75,11 +75,11 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}}[]
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}}[]
\rail@end
\end{railoutput}
@@ -220,7 +220,7 @@
exporting some result \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} yields \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -228,7 +228,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}}[]
\rail@nextbar{1}
@@ -240,7 +240,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}}[]
\rail@plus
\rail@nont{\isa{def}}[]
@@ -331,7 +331,7 @@
input process just after type checking. Also note that \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} does not support polymorphism.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}}[]
\rail@plus
\rail@plus
@@ -403,7 +403,7 @@
issuing a follow-up claim.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}}[]
\rail@plus
\rail@bar
@@ -415,7 +415,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}}[]
\rail@nextbar{1}
@@ -538,7 +538,7 @@
and assumptions, cf.\ \secref{sec:obtain}).
\begin{railoutput}
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}}[]
\rail@nextbar{1}
@@ -562,7 +562,7 @@
\rail@nont{\isa{longgoal}}[]
\rail@endbar
\rail@end
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@term{\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}}[]
\rail@nextbar{1}
@@ -574,7 +574,7 @@
\rail@endbar
\rail@nont{\isa{goal}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -849,21 +849,21 @@
assumption in the very last step.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}}[]
\rail@nont{\isa{method}}[]
\rail@bar
@@ -871,7 +871,7 @@
\rail@nont{\isa{method}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}}[]
\rail@nextbar{1}
@@ -954,14 +954,14 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.fact}{\mbox{\isa{fact}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -993,7 +993,7 @@
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
\rail@nextbar{1}
@@ -1012,15 +1012,15 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@term{\isa{del}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.of}{\mbox{\isa{of}}}}[]
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@bar
@@ -1030,7 +1030,7 @@
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@endbar
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{attribute.where}{\mbox{\isa{where}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1160,7 +1160,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}[]
\rail@nextbar{1}
@@ -1168,14 +1168,14 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}[]
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@end
@@ -1234,7 +1234,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1309,7 +1309,7 @@
occur in the conclusion.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1327,7 +1327,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
@@ -1441,7 +1441,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}}[]
\rail@nextbar{1}
@@ -1454,7 +1454,7 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.trans}{\mbox{\isa{trans}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1566,7 +1566,7 @@
later.
\begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@term{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}}[]
\rail@bar
\rail@nont{\isa{caseref}}[]
@@ -1591,14 +1591,14 @@
\rail@nont{\isa{attributes}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@plus
@@ -1606,7 +1606,7 @@
\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.params}{\mbox{\isa{params}}}}[]
\rail@plus
\rail@plus
@@ -1617,7 +1617,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1700,7 +1700,7 @@
``strengthened'' inductive statements within the object-logic.
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1721,7 +1721,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1751,7 +1751,7 @@
\rail@nont{\isa{rule}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@nont{\isa{taking}}[]
@@ -1987,15 +1987,15 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}}[]
\rail@nont{\isa{spec}}[]
\rail@end
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Tue May 03 22:28:19 2011 +0200
@@ -51,7 +51,7 @@
\begin{tabular}{rcl}
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\[0.5ex]
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\
\isa{prfx} & = & \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\
@@ -82,7 +82,7 @@
\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} \\
\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{a}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\
- \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex]
+ \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} \\
@@ -173,7 +173,7 @@
%
\begin{isamarkuptext}%
\begin{tabular}{ll}
- \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
+ \multicolumn{2}{l}{\textbf{Rules}} \\[0.5ex]
\hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{a} & rule resolved with facts (skipping ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'') \\
\hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{t} & rule instantiated with terms (skipping ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'') \\
\hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} & rule instantiated with terms, by variable name \\
--- a/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue May 03 22:28:19 2011 +0200
@@ -69,7 +69,7 @@
admissible.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{\isakeyword{imports}}}[]
@@ -145,7 +145,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{\isakeyword{begin}}}[]
@@ -220,7 +220,7 @@
available, and result names need not be given.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -232,7 +232,7 @@
\rail@nont{\isa{specs}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -249,7 +249,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -383,7 +383,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
\rail@nextbar{1}
@@ -401,7 +401,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -568,7 +568,7 @@
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
\indexisarelem{defines}\indexisarelem{notes}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
@@ -581,7 +581,7 @@
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -783,7 +783,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
@@ -791,7 +791,7 @@
\rail@nont{\isa{equations}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
@@ -799,7 +799,7 @@
\rail@nont{\isa{equations}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@bar
@@ -813,7 +813,7 @@
\rail@nont{\isa{equations}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -821,7 +821,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@end
@@ -965,7 +965,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{8}{\isa{}}
+\rail@begin{8}{}
\rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -990,7 +990,7 @@
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1001,10 +1001,10 @@
\rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1014,7 +1014,7 @@
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1022,7 +1022,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@bar
@@ -1032,10 +1032,10 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@end
\end{railoutput}
@@ -1197,7 +1197,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{5}{\isa{}}
+\rail@begin{5}{}
\rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
\rail@cr{2}
\rail@plus
@@ -1259,11 +1259,11 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@bar
\rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[]
\rail@nextbar{1}
@@ -1279,7 +1279,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1383,14 +1383,14 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1404,7 +1404,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[]
\rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
\rail@end
@@ -1453,7 +1453,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[]
\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1463,7 +1463,7 @@
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[]
\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
\rail@bar
@@ -1471,7 +1471,7 @@
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
@@ -1553,7 +1553,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -1566,7 +1566,7 @@
\rail@nextplus{2}
\rail@endplus
\rail@end
-\rail@begin{6}{\isa{}}
+\rail@begin{6}{}
\rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -1626,7 +1626,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
@@ -1634,7 +1634,7 @@
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]
\rail@nextbar{1}
@@ -1704,7 +1704,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{\isa{}}
+\rail@begin{1}{}
\rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -1743,7 +1743,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{4}{\isa{}}
+\rail@begin{4}{}
\rail@bar
\rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
\rail@nextbar{1}
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Tue May 03 22:28:19 2011 +0200
@@ -40,7 +40,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -88,7 +88,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
\rail@nextbar{1}
@@ -163,7 +163,7 @@
In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
\rail@nextbar{1}
@@ -243,7 +243,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
\rail@plus
\rail@bar
@@ -274,7 +274,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@nextbar{1}
@@ -286,14 +286,14 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
-\rail@begin{2}{\isa{}}
+\rail@begin{2}{}
\rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
\rail@plus
\rail@bar
--- a/doc-src/IsarRef/style.sty Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/IsarRef/style.sty Tue May 03 22:28:19 2011 +0200
@@ -36,15 +36,8 @@
\parindent 0pt\parskip 0.5ex
-\isabellestyle{it}
-\newcommand{\isasymdash}{\mbox{-}}
+\isabellestyle{itunderscore}
-\underscoreon
-\newcommand{\setupunderscore}{\def\isacharunderscore{\_}\def\isacharunderscorekeyword{\_}}
-\setupunderscore
-
-\makeatletter
-\def\rail@termfont{\isabellestyle{tt}\setupunderscore}
-\def\rail@nontfont{\isabellestyle{it}\setupunderscore}
-\def\rail@namefont{\isabellestyle{it}\setupunderscore}
-\makeatother
+\railtermfont{\isabellestyle{tt}}
+\railnontermfont{\isabellestyle{itunderscore}}
+\railnamefont{\isabellestyle{itunderscore}}
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue May 03 22:28:19 2011 +0200
@@ -152,7 +152,7 @@
the qualified name, for example @{text "T.length"}, where @{text T} is the
theory it is defined in, to distinguish it from the predefined @{const[source]
"List.length"}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!short_names!
+short names (no qualifiers) by setting the \verb!names_short!
configuration option in the context.
*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 03 22:28:19 2011 +0200
@@ -195,7 +195,7 @@
If there are multiple declarations of the same name, Isabelle prints
the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!short_names!
+short names (no qualifiers) by setting the \verb!names_short!
configuration option in the context.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/System/system.tex Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/System/system.tex Tue May 03 22:28:19 2011 +0200
@@ -4,6 +4,7 @@
\usepackage{../iman,../extra,../isar,../ttbox}
\usepackage[nohyphen,strings]{../underscore}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
+\usepackage{../../lib/texinputs/railsetup}
\usepackage{../IsarRef/style}
\usepackage{../pdfsetup}
--- a/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue May 03 22:28:19 2011 +0200
@@ -2,7 +2,7 @@
theory Itrev
imports Main
begin
-declare [[unique_names = false]]
+declare [[names_unique = false]]
(*>*)
section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
\index{induction heuristics|)}
*}
(*<*)
-declare [[unique_names = true]]
+declare [[names_unique = true]]
end
(*>*)
--- a/doc-src/antiquote_setup.ML Tue May 03 21:46:49 2011 +0200
+++ b/doc-src/antiquote_setup.ML Tue May 03 22:28:19 2011 +0200
@@ -19,7 +19,7 @@
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
- | "\<dash>" => "-"
+ | "\<hyphen>" => "-"
| c => c);
fun clean_name "\<dots>" = "dots"
@@ -28,7 +28,7 @@
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
(* verbatim text *)
--- a/lib/texinputs/isabelle.sty Tue May 03 21:46:49 2011 +0200
+++ b/lib/texinputs/isabelle.sty Tue May 03 22:28:19 2011 +0200
@@ -186,6 +186,14 @@
\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
}
+\newcommand{\isabellestyleitunderscore}{%
+%requires underscore.sty
+\underscoreon%
+\isabellestyleit%
+\def\isacharunderscore{\_}%
+\def\isacharunderscorekeyword{\_}%
+}
+
\newcommand{\isabellestylesl}{%
\isabellestyleit%
\def\isastyle{\small\sl}%
--- a/lib/texinputs/railsetup.sty Tue May 03 21:46:49 2011 +0200
+++ b/lib/texinputs/railsetup.sty Tue May 03 22:28:19 2011 +0200
@@ -1195,7 +1195,7 @@
% default setup for Isabelle
\newenvironment{railoutput}%
-{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\end{list}}
+{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
\def\rail@termfont{\isabellestyle{tt}}
\def\rail@nontfont{\isabellestyle{it}}
--- a/src/Pure/General/name_space.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/General/name_space.ML Tue May 03 22:28:19 2011 +0200
@@ -20,15 +20,15 @@
val markup: T -> string -> Markup.T
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
- val long_names_default: bool Unsynchronized.ref
- val long_names_raw: Config.raw
- val long_names: bool Config.T
- val short_names_default: bool Unsynchronized.ref
- val short_names_raw: Config.raw
- val short_names: bool Config.T
- val unique_names_default: bool Unsynchronized.ref
- val unique_names_raw: Config.raw
- val unique_names: bool Config.T
+ val names_long_default: bool Unsynchronized.ref
+ val names_long_raw: Config.raw
+ val names_long: bool Config.T
+ val names_short_default: bool Unsynchronized.ref
+ val names_short_raw: Config.raw
+ val names_short: bool Config.T
+ val names_unique_default: bool Unsynchronized.ref
+ val names_unique_raw: Config.raw
+ val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
val hide: bool -> string -> T -> T
val merge: T * T -> T
@@ -161,33 +161,33 @@
fun intern space xname = #1 (lookup space xname);
-val long_names_default = Unsynchronized.ref false;
-val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
-val long_names = Config.bool long_names_raw;
+val names_long_default = Unsynchronized.ref false;
+val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
+val names_long = Config.bool names_long_raw;
-val short_names_default = Unsynchronized.ref false;
-val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
-val short_names = Config.bool short_names_raw;
+val names_short_default = Unsynchronized.ref false;
+val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
+val names_short = Config.bool names_short_raw;
-val unique_names_default = Unsynchronized.ref true;
-val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
-val unique_names = Config.bool unique_names_raw;
+val names_unique_default = Unsynchronized.ref true;
+val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
+val names_unique = Config.bool names_unique_raw;
fun extern ctxt space name =
let
- val long_names = Config.get ctxt long_names;
- val short_names = Config.get ctxt short_names;
- val unique_names = Config.get ctxt unique_names;
+ val names_long = Config.get ctxt names_long;
+ val names_short = Config.get ctxt names_short;
+ val names_unique = Config.get ctxt names_unique;
fun valid require_unique xname =
let val (name', is_unique) = lookup space xname
in name = name' andalso (not require_unique orelse is_unique) end;
fun ext [] = if valid false name then name else hidden name
- | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
+ | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
in
- if long_names then name
- else if short_names then Long_Name.base_name name
+ if names_long then name
+ else if names_short then Long_Name.base_name name
else ext (get_accesses space name)
end;
--- a/src/Pure/Isar/attrib.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Tue May 03 22:28:19 2011 +0200
@@ -441,9 +441,9 @@
register_config Printer.show_question_marks_raw #>
register_config Syntax.ambiguity_level_raw #>
register_config Syntax_Trans.eta_contract_raw #>
- register_config Name_Space.long_names_raw #>
- register_config Name_Space.short_names_raw #>
- register_config Name_Space.unique_names_raw #>
+ register_config Name_Space.names_long_raw #>
+ register_config Name_Space.names_short_raw #>
+ register_config Name_Space.names_unique_raw #>
register_config ML_Context.trace_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
--- a/src/Pure/ProofGeneral/preferences.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Tue May 03 22:28:19 2011 +0200
@@ -124,7 +124,7 @@
bool_pref Goal_Display.show_consts_default
"show-consts"
"Show types of consts in Isabelle goal display",
- bool_pref Name_Space.long_names_default
+ bool_pref Name_Space.names_long_default
"long-names"
"Show fully qualified names in Isabelle terms",
bool_pref Printer.show_brackets_default
--- a/src/Pure/Thy/rail.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/Thy/rail.ML Tue May 03 22:28:19 2011 +0200
@@ -242,7 +242,8 @@
val (rail', y') = vertical_range rail 0;
val out_name =
(case name of
- Antiquote.Text s => output_text false s
+ Antiquote.Text "" => ""
+ | Antiquote.Text s => output_text false s
| Antiquote.Antiq a => output_antiq a);
in
"\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
--- a/src/Pure/Thy/thy_output.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue May 03 22:28:19 2011 +0200
@@ -450,9 +450,9 @@
val _ = add_option "show_structs" (Config.put show_structs o boolean);
val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
-val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean);
-val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
-val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
+val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
+val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
+val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
val _ = add_option "display" (Config.put display o boolean);
val _ = add_option "break" (Config.put break o boolean);
--- a/src/Pure/Tools/find_theorems.ML Tue May 03 21:46:49 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue May 03 22:28:19 2011 +0200
@@ -383,9 +383,9 @@
val shorten =
Name_Space.extern
(ctxt
- |> Config.put Name_Space.long_names false
- |> Config.put Name_Space.short_names false
- |> Config.put Name_Space.unique_names false) space;
+ |> Config.put Name_Space.names_long false
+ |> Config.put Name_Space.names_short false
+ |> Config.put Name_Space.names_unique false) space;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
nicer_name (shorten x, i) (shorten y, j)