1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 16:33:21 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 17:06:40 2011 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4      @{syntax_def antiquotation}:
     1.5        @@{antiquotation theory} options @{syntax name} |
     1.6        @@{antiquotation thm} options styles @{syntax thmrefs} |
     1.7 -      @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} |
     1.8 +      @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
     1.9        @@{antiquotation prop} options styles @{syntax prop} |
    1.10        @@{antiquotation term} options styles @{syntax term} |
    1.11        @@{antiquotation term_type} options styles @{syntax term} |
    1.12 @@ -212,7 +212,7 @@
    1.13      styles: '(' (style + ',') ')'
    1.14      ;
    1.15      style: (@{syntax name} +)
    1.16 -  "} %% FIXME check lemma
    1.17 +  "}
    1.18  
    1.19    Note that the syntax of antiquotations may \emph{not} include source
    1.20    comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim

     2.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Mon May 02 16:33:21 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Mon May 02 17:06:40 2011 +0200
     2.3 @@ -284,7 +284,7 @@
     2.4    @{rail "
     2.5      (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
     2.6        @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
     2.7 -    ( insts @{syntax thmref} | @{syntax thmrefs} )
     2.8 +    ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     2.9      ;
    2.10      @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
    2.11      ;
    2.12 @@ -295,8 +295,8 @@
    2.13      (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
    2.14      ;
    2.15  
    2.16 -    insts: ((@{syntax name} '=' @{syntax term}) + @'and') @'in'
    2.17 -  "} % FIXME check use of insts
    2.18 +    dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
    2.19 +  "}
    2.20  
    2.21  \begin{description}
    2.22  

     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 16:33:21 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 17:06:40 2011 +0200
     3.3 @@ -389,19 +389,19 @@
     3.4    \end{matharray}
     3.5  
     3.6    @{rail "
     3.7 -    @@{command (HOL) enriched_type} (prefix ':')? @{syntax term}
     3.8 +    @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
     3.9      ;
    3.10 -  "} % FIXME check prefix
    3.11 +  "}
    3.12  
    3.13    \begin{description}
    3.14  
    3.15 -  \item @{command (HOL) "enriched_type"} allows to prove and register
    3.16 -  properties about the functorial structure of type constructors;
    3.17 -  these properties then can be used by other packages to
    3.18 -  deal with those type constructors in certain type constructions.
    3.19 -  Characteristic theorems are noted in the current local theory; by
    3.20 -  default, they are prefixed with the base name of the type constructor,
    3.21 -  an explicit prefix can be given alternatively.
    3.22 +  \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
    3.23 +  prove and register properties about the functorial structure of type
    3.24 +  constructors.  These properties then can be used by other packages
    3.25 +  to deal with those type constructors in certain type constructions.
    3.26 +  Characteristic theorems are noted in the current local theory.  By
    3.27 +  default, they are prefixed with the base name of the type
    3.28 +  constructor, an explicit prefix can be given alternatively.
    3.29  
    3.30    The given term @{text "m"} is considered as \emph{mapper} for the
    3.31    corresponding type constructor and must conform to the following
    3.32 @@ -588,17 +588,18 @@
    3.33  
    3.34    @{rail "
    3.35      @@{command (HOL) partial_function} @{syntax target}?
    3.36 -      '(' mode ')' @{syntax \"fixes\"} \\ @'where' @{syntax thmdecl}? @{syntax prop}
    3.37 -  "} % FIXME check mode
    3.38 +      '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\
    3.39 +      @'where' @{syntax thmdecl}? @{syntax prop}
    3.40 +  "}
    3.41  
    3.42    \begin{description}
    3.43  
    3.44 -  \item @{command (HOL) "partial_function"} defines recursive
    3.45 -  functions based on fixpoints in complete partial orders. No
    3.46 -  termination proof is required from the user or constructed
    3.47 -  internally. Instead, the possibility of non-termination is modelled
    3.48 -  explicitly in the result type, which contains an explicit bottom
    3.49 -  element.
    3.50 +  \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines
    3.51 +  recursive functions based on fixpoints in complete partial
    3.52 +  orders. No termination proof is required from the user or
    3.53 +  constructed internally. Instead, the possibility of non-termination
    3.54 +  is modelled explicitly in the result type, which contains an
    3.55 +  explicit bottom element.
    3.56  
    3.57    Pattern matching and mutual recursion are currently not supported.
    3.58    Thus, the specification consists of a single function described by a

     4.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 16:33:21 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 17:06:40 2011 +0200
     4.3 @@ -444,7 +444,7 @@
     4.4    
     4.5      goal: (@{syntax props} + @'and')
     4.6      ;
     4.7 -    longgoal: @{syntax thmdecl}? (@{syntax contextelem} * ) conclusion
     4.8 +    longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
     4.9      ;
    4.10      conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
    4.11      ;
    4.12 @@ -458,7 +458,7 @@
    4.13    \<phi>"} to be put back into the target context.  An additional @{syntax
    4.14    context} specification may build up an initial proof context for the
    4.15    subsequent claim; this includes local definitions and syntax as
    4.16 -  well, see the definition of @{syntax contextelem} in
    4.17 +  well, see the definition of @{syntax context_elem} in
    4.18    \secref{sec:locale}.
    4.19    
    4.20    \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
    4.21 @@ -1278,7 +1278,7 @@
    4.22      ;
    4.23      @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    4.24      ;
    4.25 -    @@{method coinduct} insts taking rule?
    4.26 +    @@{method coinduct} @{syntax insts} taking rule?
    4.27      ;
    4.28  
    4.29      rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
    4.30 @@ -1289,7 +1289,7 @@
    4.31      ;
    4.32      arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
    4.33      ;
    4.34 -    taking: 'taking' ':' insts
    4.35 +    taking: 'taking' ':' @{syntax insts}
    4.36    "}
    4.37  
    4.38    \begin{description}

     5.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 16:33:21 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 17:06:40 2011 +0200
     5.3 @@ -311,15 +311,15 @@
     5.4    duplicate declarations.
     5.5  
     5.6    @{rail "
     5.7 -    @{syntax_def localeexpr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
     5.8 +    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
     5.9      ;
    5.10 -    instance: (qualifier ':')? @{syntax nameref} (posinsts | namedinsts)
    5.11 +    instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
    5.12      ;
    5.13      qualifier: @{syntax name} ('?' | '!')?
    5.14      ;
    5.15 -    posinsts: ('_' | @{syntax term})*
    5.16 +    pos_insts: ('_' | @{syntax term})*
    5.17      ;
    5.18 -    namedinsts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
    5.19 +    named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
    5.20    "}
    5.21  
    5.22    A locale instance consists of a reference to a locale and either
    5.23 @@ -364,10 +364,10 @@
    5.24      ;
    5.25      @@{command print_locale} '!'? @{syntax nameref}
    5.26      ;
    5.27 -    @{syntax_def locale}: @{syntax contextelem}+ |
    5.28 -      @{syntax localeexpr} ('+' (@{syntax contextelem}+))?
    5.29 +    @{syntax_def locale}: @{syntax context_elem}+ |
    5.30 +      @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
    5.31      ;
    5.32 -    @{syntax_def contextelem}:
    5.33 +    @{syntax_def context_elem}:
    5.34        @'fixes' (@{syntax \"fixes\"} + @'and') |
    5.35        @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
    5.36        @'assumes' (@{syntax props} + @'and') |
    5.37 @@ -499,13 +499,13 @@
    5.38    \end{matharray}
    5.39  
    5.40    @{rail "
    5.41 -    @@{command interpretation} @{syntax localeexpr} equations?
    5.42 +    @@{command interpretation} @{syntax locale_expr} equations?
    5.43      ;
    5.44 -    @@{command interpret} @{syntax localeexpr} equations?
    5.45 +    @@{command interpret} @{syntax locale_expr} equations?
    5.46      ;
    5.47 -    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax localeexpr} equations?
    5.48 +    @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} equations?
    5.49      ;
    5.50 -    @@{command print_dependencies} '!'? @{syntax localeexpr}
    5.51 +    @@{command print_dependencies} '!'? @{syntax locale_expr}
    5.52      ;
    5.53      @@{command print_interps} @{syntax nameref}
    5.54      ;
    5.55 @@ -640,8 +640,8 @@
    5.56  
    5.57    @{rail "
    5.58      @@{command class} @{syntax name} '='
    5.59 -      ((superclassexpr '+' (@{syntax contextelem}+)) |
    5.60 -        superclassexpr | (@{syntax contextelem}+)) \\
    5.61 +      ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
    5.62 +        @{syntax nameref} | (@{syntax context_elem}+)) \\
    5.63        @'begin'?
    5.64      ;
    5.65      @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
    5.66 @@ -658,9 +658,7 @@
    5.67      ;
    5.68      @@{command class_deps}
    5.69      ;
    5.70 -
    5.71 -    superclassexpr: @{syntax nameref} | (@{syntax nameref} '+' superclassexpr)
    5.72 -  "}  %% FIXME check superclassexpr
    5.73 +  "}
    5.74  
    5.75    \begin{description}
    5.76  
    5.77 @@ -821,9 +819,9 @@
    5.78  
    5.79    @{rail "
    5.80      @@{command overloading} \\
    5.81 -    ( @{syntax string} ( '==' | '\<equiv>' ) @{syntax term}
    5.82 +    ( @{syntax name} ( '==' | '\<equiv>' ) @{syntax term}
    5.83      ( '(' @'unchecked' ')' )? +) @'begin'
    5.84 -  "}  %% FIXME check string vs. name
    5.85 +  "}
    5.86  
    5.87    \begin{description}
    5.88  

     6.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon May 02 16:33:21 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon May 02 17:06:40 2011 +0200
     6.3 @@ -235,7 +235,7 @@
     6.4  \rail@nont{\isa{antiquotation}}[]
     6.5  \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
     6.6  \rail@end
     6.7 -\rail@begin{21}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
     6.8 +\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
     6.9  \rail@bar
    6.10  \rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
    6.11  \rail@nont{\isa{options}}[]
    6.12 @@ -251,77 +251,81 @@
    6.13  \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
    6.14  \rail@term{\isa{\isakeyword{by}}}[]
    6.15  \rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
    6.16 +\rail@bar
    6.17  \rail@nextbar{3}
    6.18 +\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
    6.19 +\rail@endbar
    6.20 +\rail@nextbar{4}
    6.21  \rail@term{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}}[]
    6.22  \rail@nont{\isa{options}}[]
    6.23  \rail@nont{\isa{styles}}[]
    6.24  \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
    6.25 -\rail@nextbar{4}
    6.26 +\rail@nextbar{5}
    6.27  \rail@term{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}}[]
    6.28  \rail@nont{\isa{options}}[]
    6.29  \rail@nont{\isa{styles}}[]
    6.30  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    6.31 -\rail@nextbar{5}
    6.32 +\rail@nextbar{6}
    6.33  \rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
    6.34  \rail@nont{\isa{options}}[]
    6.35  \rail@nont{\isa{styles}}[]
    6.36  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    6.37 -\rail@nextbar{6}
    6.38 +\rail@nextbar{7}
    6.39  \rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
    6.40  \rail@nont{\isa{options}}[]
    6.41  \rail@nont{\isa{styles}}[]
    6.42  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    6.43 -\rail@nextbar{7}
    6.44 +\rail@nextbar{8}
    6.45  \rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
    6.46  \rail@nont{\isa{options}}[]
    6.47  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    6.48 -\rail@nextbar{8}
    6.49 +\rail@nextbar{9}
    6.50  \rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
    6.51  \rail@nont{\isa{options}}[]
    6.52  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    6.53 -\rail@nextbar{9}
    6.54 +\rail@nextbar{10}
    6.55  \rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
    6.56  \rail@nont{\isa{options}}[]
    6.57  \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
    6.58 -\rail@nextbar{10}
    6.59 +\rail@nextbar{11}
    6.60  \rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
    6.61  \rail@nont{\isa{options}}[]
    6.62  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    6.63 -\rail@nextbar{11}
    6.64 +\rail@nextbar{12}
    6.65  \rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
    6.66  \rail@nont{\isa{options}}[]
    6.67  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    6.68 -\rail@nextbar{12}
    6.69 +\rail@nextbar{13}
    6.70  \rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
    6.71  \rail@nont{\isa{options}}[]
    6.72  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    6.73 -\rail@nextbar{13}
    6.74 +\rail@nextbar{14}
    6.75  \rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
    6.76  \rail@nont{\isa{options}}[]
    6.77 -\rail@nextbar{14}
    6.78 +\rail@nextbar{15}
    6.79  \rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
    6.80  \rail@nont{\isa{options}}[]
    6.81 -\rail@nextbar{15}
    6.82 +\rail@nextbar{16}
    6.83  \rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
    6.84  \rail@nont{\isa{options}}[]
    6.85  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    6.86 -\rail@nextbar{16}
    6.87 +\rail@nextbar{17}
    6.88  \rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
    6.89  \rail@nont{\isa{options}}[]
    6.90  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    6.91 -\rail@nextbar{17}
    6.92 +\rail@nextbar{18}
    6.93  \rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
    6.94  \rail@nont{\isa{options}}[]
    6.95  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    6.96 -\rail@nextbar{18}
    6.97 +\rail@nextbar{19}
    6.98  \rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
    6.99  \rail@nont{\isa{options}}[]
   6.100  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   6.101 -\rail@nextbar{19}
   6.102 +\rail@nextbar{20}
   6.103  \rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
   6.104  \rail@nont{\isa{options}}[]
   6.105  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   6.106 -\rail@nextbar{20}
   6.107 +\rail@nextbar{21}
   6.108  \rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
   6.109  \rail@nont{\isa{options}}[]
   6.110  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   6.111 @@ -364,7 +368,7 @@
   6.112  \rail@endplus
   6.113  \rail@end
   6.114  \end{railoutput}
   6.115 - %% FIXME check lemma
   6.116 +
   6.117  
   6.118    Note that the syntax of antiquotations may \emph{not} include source
   6.119    comments \verb|(*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*)| nor verbatim

     7.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon May 02 16:33:21 2011 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon May 02 17:06:40 2011 +0200
     7.3 @@ -419,7 +419,8 @@
     7.4  \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
     7.5  \rail@endbar
     7.6  \rail@bar
     7.7 -\rail@nont{\isa{insts}}[]
     7.8 +\rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
     7.9 +\rail@term{\isa{\isakeyword{in}}}[]
    7.10  \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
    7.11  \rail@nextbar{1}
    7.12  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    7.13 @@ -466,7 +467,7 @@
    7.14  \rail@endbar
    7.15  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
    7.16  \rail@end
    7.17 -\rail@begin{2}{\isa{insts}}
    7.18 +\rail@begin{2}{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}
    7.19  \rail@plus
    7.20  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    7.21  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
    7.22 @@ -474,10 +475,9 @@
    7.23  \rail@nextplus{1}
    7.24  \rail@cterm{\isa{\isakeyword{and}}}[]
    7.25  \rail@endplus
    7.26 -\rail@term{\isa{\isakeyword{in}}}[]
    7.27  \rail@end
    7.28  \end{railoutput}
    7.29 - % FIXME check use of insts
    7.30 +
    7.31  
    7.32  \begin{description}
    7.33  

     8.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 16:33:21 2011 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 17:06:40 2011 +0200
     8.3 @@ -503,23 +503,23 @@
     8.4  \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
     8.5  \rail@bar
     8.6  \rail@nextbar{1}
     8.7 -\rail@nont{\isa{prefix}}[]
     8.8 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
     8.9  \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
    8.10  \rail@endbar
    8.11  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    8.12  \rail@end
    8.13  \end{railoutput}
    8.14 - % FIXME check prefix
    8.15 +
    8.16  
    8.17    \begin{description}
    8.18  
    8.19 -  \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register
    8.20 -  properties about the functorial structure of type constructors;
    8.21 -  these properties then can be used by other packages to
    8.22 -  deal with those type constructors in certain type constructions.
    8.23 -  Characteristic theorems are noted in the current local theory; by
    8.24 -  default, they are prefixed with the base name of the type constructor,
    8.25 -  an explicit prefix can be given alternatively.
    8.26 +  \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
    8.27 +  prove and register properties about the functorial structure of type
    8.28 +  constructors.  These properties then can be used by other packages
    8.29 +  to deal with those type constructors in certain type constructions.
    8.30 +  Characteristic theorems are noted in the current local theory.  By
    8.31 +  default, they are prefixed with the base name of the type
    8.32 +  constructor, an explicit prefix can be given alternatively.
    8.33  
    8.34    The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the
    8.35    corresponding type constructor and must conform to the following
    8.36 @@ -788,7 +788,7 @@
    8.37  \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
    8.38  \rail@endbar
    8.39  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    8.40 -\rail@nont{\isa{mode}}[]
    8.41 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
    8.42  \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    8.43  \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
    8.44  \rail@cr{3}
    8.45 @@ -800,16 +800,16 @@
    8.46  \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
    8.47  \rail@end
    8.48  \end{railoutput}
    8.49 - % FIXME check mode
    8.50 +
    8.51  
    8.52    \begin{description}
    8.53  
    8.54 -  \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}} defines recursive
    8.55 -  functions based on fixpoints in complete partial orders. No
    8.56 -  termination proof is required from the user or constructed
    8.57 -  internally. Instead, the possibility of non-termination is modelled
    8.58 -  explicitly in the result type, which contains an explicit bottom
    8.59 -  element.
    8.60 +  \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
    8.61 +  recursive functions based on fixpoints in complete partial
    8.62 +  orders. No termination proof is required from the user or
    8.63 +  constructed internally. Instead, the possibility of non-termination
    8.64 +  is modelled explicitly in the result type, which contains an
    8.65 +  explicit bottom element.
    8.66  
    8.67    Pattern matching and mutual recursion are currently not supported.
    8.68    Thus, the specification consists of a single function described by a

     9.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon May 02 16:33:21 2011 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon May 02 17:06:40 2011 +0200
     9.3 @@ -596,7 +596,7 @@
     9.4  \rail@endbar
     9.5  \rail@plus
     9.6  \rail@nextplus{1}
     9.7 -\rail@cnont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
     9.8 +\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
     9.9  \rail@endplus
    9.10  \rail@nont{\isa{conclusion}}[]
    9.11  \rail@end
    9.12 @@ -638,7 +638,7 @@
    9.13    \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
    9.14    \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
    9.15    subsequent claim; this includes local definitions and syntax as
    9.16 -  well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
    9.17 +  well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
    9.18    \secref{sec:locale}.
    9.19    
    9.20    \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
    9.21 @@ -1753,7 +1753,7 @@
    9.22  \rail@end
    9.23  \rail@begin{2}{\isa{}}
    9.24  \rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
    9.25 -\rail@nont{\isa{insts}}[]
    9.26 +\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
    9.27  \rail@nont{\isa{taking}}[]
    9.28  \rail@bar
    9.29  \rail@nextbar{1}
    9.30 @@ -1821,7 +1821,7 @@
    9.31  \rail@begin{1}{\isa{taking}}
    9.32  \rail@term{\isa{taking}}[]
    9.33  \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
    9.34 -\rail@nont{\isa{insts}}[]
    9.35 +\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
    9.36  \rail@end
    9.37  \end{railoutput}
    9.38  

    10.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon May 02 16:33:21 2011 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon May 02 17:06:40 2011 +0200
    10.3 @@ -470,7 +470,7 @@
    10.4    duplicate declarations.
    10.5  
    10.6    \begin{railoutput}
    10.7 -\rail@begin{3}{\indexdef{}{syntax}{localeexpr}\hypertarget{syntax.localeexpr}{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}}
    10.8 +\rail@begin{3}{\indexdef{}{syntax}{locale\_expr}\hypertarget{syntax.locale-expr}{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}}
    10.9  \rail@plus
   10.10  \rail@nont{\isa{instance}}[]
   10.11  \rail@nextplus{1}
   10.12 @@ -494,9 +494,9 @@
   10.13  \rail@endbar
   10.14  \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   10.15  \rail@bar
   10.16 -\rail@nont{\isa{posinsts}}[]
   10.17 +\rail@nont{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}[]
   10.18  \rail@nextbar{1}
   10.19 -\rail@nont{\isa{namedinsts}}[]
   10.20 +\rail@nont{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}[]
   10.21  \rail@endbar
   10.22  \rail@end
   10.23  \rail@begin{3}{\isa{qualifier}}
   10.24 @@ -510,7 +510,7 @@
   10.25  \rail@endbar
   10.26  \rail@endbar
   10.27  \rail@end
   10.28 -\rail@begin{3}{\isa{posinsts}}
   10.29 +\rail@begin{3}{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}
   10.30  \rail@plus
   10.31  \rail@nextplus{1}
   10.32  \rail@bar
   10.33 @@ -520,7 +520,7 @@
   10.34  \rail@endbar
   10.35  \rail@endplus
   10.36  \rail@end
   10.37 -\rail@begin{2}{\isa{namedinsts}}
   10.38 +\rail@begin{2}{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}
   10.39  \rail@term{\isa{\isakeyword{where}}}[]
   10.40  \rail@plus
   10.41  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   10.42 @@ -596,22 +596,22 @@
   10.43  \rail@begin{5}{\indexdef{}{syntax}{locale}\hypertarget{syntax.locale}{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}}
   10.44  \rail@bar
   10.45  \rail@plus
   10.46 -\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
   10.47 +\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
   10.48  \rail@nextplus{1}
   10.49  \rail@endplus
   10.50  \rail@nextbar{2}
   10.51 -\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
   10.52 +\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
   10.53  \rail@bar
   10.54  \rail@nextbar{3}
   10.55  \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
   10.56  \rail@plus
   10.57 -\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
   10.58 +\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
   10.59  \rail@nextplus{4}
   10.60  \rail@endplus
   10.61  \rail@endbar
   10.62  \rail@endbar
   10.63  \rail@end
   10.64 -\rail@begin{12}{\indexdef{}{syntax}{contextelem}\hypertarget{syntax.contextelem}{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}}
   10.65 +\rail@begin{12}{\indexdef{}{syntax}{context\_elem}\hypertarget{syntax.context-elem}{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}}
   10.66  \rail@bar
   10.67  \rail@term{\isa{\isakeyword{fixes}}}[]
   10.68  \rail@plus
   10.69 @@ -789,7 +789,7 @@
   10.70    \begin{railoutput}
   10.71  \rail@begin{2}{\isa{}}
   10.72  \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
   10.73 -\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
   10.74 +\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
   10.75  \rail@bar
   10.76  \rail@nextbar{1}
   10.77  \rail@nont{\isa{equations}}[]
   10.78 @@ -797,7 +797,7 @@
   10.79  \rail@end
   10.80  \rail@begin{2}{\isa{}}
   10.81  \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
   10.82 -\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
   10.83 +\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
   10.84  \rail@bar
   10.85  \rail@nextbar{1}
   10.86  \rail@nont{\isa{equations}}[]
   10.87 @@ -811,7 +811,7 @@
   10.88  \rail@nextbar{1}
   10.89  \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
   10.90  \rail@endbar
   10.91 -\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
   10.92 +\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
   10.93  \rail@bar
   10.94  \rail@nextbar{1}
   10.95  \rail@nont{\isa{equations}}[]
   10.96 @@ -823,7 +823,7 @@
   10.97  \rail@nextbar{1}
   10.98  \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
   10.99  \rail@endbar
  10.100 -\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
  10.101 +\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
  10.102  \rail@end
  10.103  \rail@begin{1}{\isa{}}
  10.104  \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
  10.105 @@ -974,17 +974,17 @@
  10.106  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  10.107  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
  10.108  \rail@bar
  10.109 -\rail@nont{\isa{superclassexpr}}[]
  10.110 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  10.111  \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
  10.112  \rail@plus
  10.113 -\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
  10.114 +\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
  10.115  \rail@nextplus{1}
  10.116  \rail@endplus
  10.117  \rail@nextbar{2}
  10.118 -\rail@nont{\isa{superclassexpr}}[]
  10.119 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  10.120  \rail@nextbar{3}
  10.121  \rail@plus
  10.122 -\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
  10.123 +\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
  10.124  \rail@nextplus{4}
  10.125  \rail@endplus
  10.126  \rail@endbar
  10.127 @@ -1042,17 +1042,8 @@
  10.128  \rail@begin{1}{\isa{}}
  10.129  \rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
  10.130  \rail@end
  10.131 -\rail@begin{2}{\isa{superclassexpr}}
  10.132 -\rail@bar
  10.133 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  10.134 -\rail@nextbar{1}
  10.135 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  10.136 -\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
  10.137 -\rail@nont{\isa{superclassexpr}}[]
  10.138 -\rail@endbar
  10.139 -\rail@end
  10.140  \end{railoutput}
  10.141 -  %% FIXME check superclassexpr
  10.142 +
  10.143  
  10.144    \begin{description}
  10.145  
  10.146 @@ -1214,7 +1205,7 @@
  10.147  \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
  10.148  \rail@cr{2}
  10.149  \rail@plus
  10.150 -\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
  10.151 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  10.152  \rail@bar
  10.153  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
  10.154  \rail@nextbar{3}
  10.155 @@ -1232,7 +1223,7 @@
  10.156  \rail@term{\isa{\isakeyword{begin}}}[]
  10.157  \rail@end
  10.158  \end{railoutput}
  10.159 -  %% FIXME check string vs. name
  10.160 +
  10.161  
  10.162    \begin{description}
  10.163