# HG changeset patch
# User wenzelm
# Date 1304348800 -7200
# Node ID 77d239840285d675353f1531e4eb1f2d4807d34b
# Parent  92715b528e78829f52b253d6f9a0bc2aca261404
more precise rail diagrams;
misc tuning;

diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/Document_Preparation.thy
--- 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
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/Generic.thy
--- 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}
 
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/Proof.thy
--- 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}
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/Spec.thy
--- 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}
 
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- 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
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/document/Generic.tex
--- 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}
 
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/document/Proof.tex
--- 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}
 
diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/document/Spec.tex
--- 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}