--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 17:06:40 2011 +0200
@@ -185,7 +185,7 @@
@{syntax_def antiquotation}:
@@{antiquotation theory} options @{syntax name} |
@@{antiquotation thm} options styles @{syntax thmrefs} |
- @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} |
+ @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
@@{antiquotation term_type} options styles @{syntax term} |
@@ -212,7 +212,7 @@
styles: '(' (style + ',') ')'
;
style: (@{syntax name} +)
- "} %% FIXME check lemma
+ "}
Note that the syntax of antiquotations may \emph{not} include source
comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
--- a/doc-src/IsarRef/Thy/Generic.thy Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon May 02 17:06:40 2011 +0200
@@ -284,7 +284,7 @@
@{rail "
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
@@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
- ( insts @{syntax thmref} | @{syntax thmrefs} )
+ ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
@@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
;
@@ -295,8 +295,8 @@
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
;
- insts: ((@{syntax name} '=' @{syntax term}) + @'and') @'in'
- "} % FIXME check use of insts
+ dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
+ "}
\begin{description}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 17:06:40 2011 +0200
@@ -389,19 +389,19 @@
\end{matharray}
@{rail "
- @@{command (HOL) enriched_type} (prefix ':')? @{syntax term}
+ @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
;
- "} % FIXME check prefix
+ "}
\begin{description}
- \item @{command (HOL) "enriched_type"} allows to prove and register
- properties about the functorial structure of type constructors;
- these properties then can be used by other packages to
- deal with those type constructors in certain type constructions.
- Characteristic theorems are noted in the current local theory; by
- default, they are prefixed with the base name of the type constructor,
- an explicit prefix can be given alternatively.
+ \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
+ prove and register properties about the functorial structure of type
+ constructors. These properties then can be used by other packages
+ to deal with those type constructors in certain type constructions.
+ Characteristic theorems are noted in the current local theory. By
+ default, they are prefixed with the base name of the type
+ constructor, an explicit prefix can be given alternatively.
The given term @{text "m"} is considered as \emph{mapper} for the
corresponding type constructor and must conform to the following
@@ -588,17 +588,18 @@
@{rail "
@@{command (HOL) partial_function} @{syntax target}?
- '(' mode ')' @{syntax \"fixes\"} \\ @'where' @{syntax thmdecl}? @{syntax prop}
- "} % FIXME check mode
+ '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\
+ @'where' @{syntax thmdecl}? @{syntax prop}
+ "}
\begin{description}
- \item @{command (HOL) "partial_function"} defines recursive
- functions based on fixpoints in complete partial orders. No
- termination proof is required from the user or constructed
- internally. Instead, the possibility of non-termination is modelled
- explicitly in the result type, which contains an explicit bottom
- element.
+ \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines
+ recursive functions based on fixpoints in complete partial
+ orders. No termination proof is required from the user or
+ constructed internally. Instead, the possibility of non-termination
+ is modelled explicitly in the result type, which contains an
+ explicit bottom element.
Pattern matching and mutual recursion are currently not supported.
Thus, the specification consists of a single function described by a
--- a/doc-src/IsarRef/Thy/Proof.thy Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon May 02 17:06:40 2011 +0200
@@ -444,7 +444,7 @@
goal: (@{syntax props} + @'and')
;
- longgoal: @{syntax thmdecl}? (@{syntax contextelem} * ) conclusion
+ longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
;
conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
;
@@ -458,7 +458,7 @@
\<phi>"} to be put back into the target context. An additional @{syntax
context} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of @{syntax contextelem} in
+ well, see the definition of @{syntax context_elem} in
\secref{sec:locale}.
\item @{command "theorem"}~@{text "a: \<phi>"} and @{command
@@ -1278,7 +1278,7 @@
;
@@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
;
- @@{method coinduct} insts taking rule?
+ @@{method coinduct} @{syntax insts} taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
@@ -1289,7 +1289,7 @@
;
arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
;
- taking: 'taking' ':' insts
+ taking: 'taking' ':' @{syntax insts}
"}
\begin{description}
--- a/doc-src/IsarRef/Thy/Spec.thy Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon May 02 17:06:40 2011 +0200
@@ -311,15 +311,15 @@
duplicate declarations.
@{rail "
- @{syntax_def localeexpr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
+ @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
;
- instance: (qualifier ':')? @{syntax nameref} (posinsts | namedinsts)
+ instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
;
qualifier: @{syntax name} ('?' | '!')?
;
- posinsts: ('_' | @{syntax term})*
+ pos_insts: ('_' | @{syntax term})*
;
- namedinsts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
+ named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
"}
A locale instance consists of a reference to a locale and either
@@ -364,10 +364,10 @@
;
@@{command print_locale} '!'? @{syntax nameref}
;
- @{syntax_def locale}: @{syntax contextelem}+ |
- @{syntax localeexpr} ('+' (@{syntax contextelem}+))?
+ @{syntax_def locale}: @{syntax context_elem}+ |
+ @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
;
- @{syntax_def contextelem}:
+ @{syntax_def context_elem}:
@'fixes' (@{syntax \"fixes\"} + @'and') |
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
@'assumes' (@{syntax props} + @'and') |
@@ -499,13 +499,13 @@
\end{matharray}
@{rail "
- @@{command interpretation} @{syntax localeexpr} equations?
+ @@{command interpretation} @{syntax locale_expr} equations?
;
- @@{command interpret} @{syntax localeexpr} equations?
+ @@{command interpret} @{syntax locale_expr} equations?
;
- @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax localeexpr} equations?
+ @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} equations?
;
- @@{command print_dependencies} '!'? @{syntax localeexpr}
+ @@{command print_dependencies} '!'? @{syntax locale_expr}
;
@@{command print_interps} @{syntax nameref}
;
@@ -640,8 +640,8 @@
@{rail "
@@{command class} @{syntax name} '='
- ((superclassexpr '+' (@{syntax contextelem}+)) |
- superclassexpr | (@{syntax contextelem}+)) \\
+ ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
+ @{syntax nameref} | (@{syntax context_elem}+)) \\
@'begin'?
;
@@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
@@ -658,9 +658,7 @@
;
@@{command class_deps}
;
-
- superclassexpr: @{syntax nameref} | (@{syntax nameref} '+' superclassexpr)
- "} %% FIXME check superclassexpr
+ "}
\begin{description}
@@ -821,9 +819,9 @@
@{rail "
@@{command overloading} \\
- ( @{syntax string} ( '==' | '\<equiv>' ) @{syntax term}
+ ( @{syntax name} ( '==' | '\<equiv>' ) @{syntax term}
( '(' @'unchecked' ')' )? +) @'begin'
- "} %% FIXME check string vs. name
+ "}
\begin{description}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 17:06:40 2011 +0200
@@ -235,7 +235,7 @@
\rail@nont{\isa{antiquotation}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{21}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
+\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
\rail@bar
\rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
\rail@nont{\isa{options}}[]
@@ -251,77 +251,81 @@
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@term{\isa{\isakeyword{by}}}[]
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
+\rail@bar
\rail@nextbar{3}
+\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
+\rail@endbar
+\rail@nextbar{4}
\rail@term{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextbar{4}
+\rail@nextbar{5}
\rail@term{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{5}
+\rail@nextbar{6}
\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\isa{styles}}[]
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{7}
+\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\isa{styles}}[]
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextbar{8}
\rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{8}
+\rail@nextbar{9}
\rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{9}
+\rail@nextbar{10}
\rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
-\rail@nextbar{10}
+\rail@nextbar{11}
\rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{11}
+\rail@nextbar{12}
\rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{12}
-\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextbar{13}
+\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{14}
\rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{14}
+\rail@nextbar{15}
\rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{15}
+\rail@nextbar{16}
\rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{16}
+\rail@nextbar{17}
\rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{17}
+\rail@nextbar{18}
\rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{18}
+\rail@nextbar{19}
\rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{19}
+\rail@nextbar{20}
\rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{20}
+\rail@nextbar{21}
\rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -364,7 +368,7 @@
\rail@endplus
\rail@end
\end{railoutput}
- %% FIXME check lemma
+
Note that the syntax of antiquotations may \emph{not} include source
comments \verb|(*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*)| nor verbatim
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 17:06:40 2011 +0200
@@ -419,7 +419,8 @@
\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
\rail@endbar
\rail@bar
-\rail@nont{\isa{insts}}[]
+\rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
+\rail@term{\isa{\isakeyword{in}}}[]
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
@@ -466,7 +467,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
-\rail@begin{2}{\isa{insts}}
+\rail@begin{2}{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -474,10 +475,9 @@
\rail@nextplus{1}
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
-\rail@term{\isa{\isakeyword{in}}}[]
\rail@end
\end{railoutput}
- % FIXME check use of insts
+
\begin{description}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 17:06:40 2011 +0200
@@ -503,23 +503,23 @@
\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{prefix}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
\end{railoutput}
- % FIXME check prefix
+
\begin{description}
- \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register
- properties about the functorial structure of type constructors;
- these properties then can be used by other packages to
- deal with those type constructors in certain type constructions.
- Characteristic theorems are noted in the current local theory; by
- default, they are prefixed with the base name of the type constructor,
- an explicit prefix can be given alternatively.
+ \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to
+ prove and register properties about the functorial structure of type
+ constructors. These properties then can be used by other packages
+ to deal with those type constructors in certain type constructions.
+ Characteristic theorems are noted in the current local theory. By
+ default, they are prefixed with the base name of the type
+ constructor, an explicit prefix can be given alternatively.
The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the
corresponding type constructor and must conform to the following
@@ -788,7 +788,7 @@
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
\rail@endbar
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@nont{\isa{mode}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
\rail@cr{3}
@@ -800,16 +800,16 @@
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@end
\end{railoutput}
- % FIXME check mode
+
\begin{description}
- \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}} defines recursive
- functions based on fixpoints in complete partial orders. No
- termination proof is required from the user or constructed
- internally. Instead, the possibility of non-termination is modelled
- explicitly in the result type, which contains an explicit bottom
- element.
+ \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines
+ recursive functions based on fixpoints in complete partial
+ orders. No termination proof is required from the user or
+ constructed internally. Instead, the possibility of non-termination
+ is modelled explicitly in the result type, which contains an
+ explicit bottom element.
Pattern matching and mutual recursion are currently not supported.
Thus, the specification consists of a single function described by a
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 17:06:40 2011 +0200
@@ -596,7 +596,7 @@
\rail@endbar
\rail@plus
\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@endplus
\rail@nont{\isa{conclusion}}[]
\rail@end
@@ -638,7 +638,7 @@
\item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context. An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
+ well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
\secref{sec:locale}.
\item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as
@@ -1753,7 +1753,7 @@
\rail@end
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
-\rail@nont{\isa{insts}}[]
+\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@nont{\isa{taking}}[]
\rail@bar
\rail@nextbar{1}
@@ -1821,7 +1821,7 @@
\rail@begin{1}{\isa{taking}}
\rail@term{\isa{taking}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
-\rail@nont{\isa{insts}}[]
+\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@end
\end{railoutput}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 17:06:40 2011 +0200
@@ -470,7 +470,7 @@
duplicate declarations.
\begin{railoutput}
-\rail@begin{3}{\indexdef{}{syntax}{localeexpr}\hypertarget{syntax.localeexpr}{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}}
+\rail@begin{3}{\indexdef{}{syntax}{locale\_expr}\hypertarget{syntax.locale-expr}{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}}
\rail@plus
\rail@nont{\isa{instance}}[]
\rail@nextplus{1}
@@ -494,9 +494,9 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@bar
-\rail@nont{\isa{posinsts}}[]
+\rail@nont{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}[]
\rail@nextbar{1}
-\rail@nont{\isa{namedinsts}}[]
+\rail@nont{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}[]
\rail@endbar
\rail@end
\rail@begin{3}{\isa{qualifier}}
@@ -510,7 +510,7 @@
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{posinsts}}
+\rail@begin{3}{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@plus
\rail@nextplus{1}
\rail@bar
@@ -520,7 +520,7 @@
\rail@endbar
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{namedinsts}}
+\rail@begin{2}{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@term{\isa{\isakeyword{where}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -596,22 +596,22 @@
\rail@begin{5}{\indexdef{}{syntax}{locale}\hypertarget{syntax.locale}{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}}
\rail@bar
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@nextbar{2}
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{3}
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{4}
\rail@endplus
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{12}{\indexdef{}{syntax}{contextelem}\hypertarget{syntax.contextelem}{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}}
+\rail@begin{12}{\indexdef{}{syntax}{context\_elem}\hypertarget{syntax.context-elem}{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}}
\rail@bar
\rail@term{\isa{\isakeyword{fixes}}}[]
\rail@plus
@@ -789,7 +789,7 @@
\begin{railoutput}
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -797,7 +797,7 @@
\rail@end
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -811,7 +811,7 @@
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
\rail@endbar
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -823,7 +823,7 @@
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
\rail@endbar
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@end
\rail@begin{1}{\isa{}}
\rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
@@ -974,17 +974,17 @@
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@bar
-\rail@nont{\isa{superclassexpr}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@nextbar{2}
-\rail@nont{\isa{superclassexpr}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@nextbar{3}
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{4}
\rail@endplus
\rail@endbar
@@ -1042,17 +1042,8 @@
\rail@begin{1}{\isa{}}
\rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@end
-\rail@begin{2}{\isa{superclassexpr}}
-\rail@bar
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
-\rail@nont{\isa{superclassexpr}}[]
-\rail@endbar
-\rail@end
\end{railoutput}
- %% FIXME check superclassexpr
+
\begin{description}
@@ -1214,7 +1205,7 @@
\rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
\rail@cr{2}
\rail@plus
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
\rail@nextbar{3}
@@ -1232,7 +1223,7 @@
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
\end{railoutput}
- %% FIXME check string vs. name
+
\begin{description}