updated generated files;
authorwenzelm
Thu Feb 26 20:55:47 2009 +0100 (2009-02-26)
changeset 301215c7bcb296600
parent 30120 aaa4667285c8
child 30122 1c912a9d8200
updated generated files;
doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
doc-src/IsarImplementation/Thy/document/Integration.tex
doc-src/IsarImplementation/Thy/document/Local_Theory.tex
doc-src/IsarImplementation/Thy/document/Logic.tex
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/Prelim.tex
doc-src/IsarImplementation/Thy/document/Proof.tex
doc-src/IsarImplementation/Thy/document/Tactic.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 20:44:07 2009 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 20:55:47 2009 +0100
     1.3 @@ -1153,7 +1153,7 @@
     1.4  \hspace*{0pt}module Example where {\char123}\\
     1.5  \hspace*{0pt}\\
     1.6  \hspace*{0pt}\\
     1.7 -\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
     1.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
     1.9  \hspace*{0pt}\\
    1.10  \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    1.11  \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    1.12 @@ -1240,7 +1240,7 @@
    1.13  \hspace*{0pt}structure Example = \\
    1.14  \hspace*{0pt}struct\\
    1.15  \hspace*{0pt}\\
    1.16 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    1.17 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    1.18  \hspace*{0pt}\\
    1.19  \hspace*{0pt}fun nat{\char95}aux i n =\\
    1.20  \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 20:44:07 2009 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 20:55:47 2009 +0100
     2.3 @@ -267,9 +267,9 @@
     2.4  \hspace*{0pt}structure Example = \\
     2.5  \hspace*{0pt}struct\\
     2.6  \hspace*{0pt}\\
     2.7 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
     2.8 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
     2.9  \hspace*{0pt}\\
    2.10 -\hspace*{0pt}datatype boola = False | True;\\
    2.11 +\hspace*{0pt}datatype boola = True | False;\\
    2.12  \hspace*{0pt}\\
    2.13  \hspace*{0pt}fun anda x True = x\\
    2.14  \hspace*{0pt} ~| anda x False = False\\
    2.15 @@ -350,7 +350,7 @@
    2.16  \hspace*{0pt}structure Example = \\
    2.17  \hspace*{0pt}struct\\
    2.18  \hspace*{0pt}\\
    2.19 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    2.20 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    2.21  \hspace*{0pt}\\
    2.22  \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    2.23  \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
    2.24 @@ -407,7 +407,7 @@
    2.25  \hspace*{0pt}structure Example = \\
    2.26  \hspace*{0pt}struct\\
    2.27  \hspace*{0pt}\\
    2.28 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    2.29 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    2.30  \hspace*{0pt}\\
    2.31  \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    2.32  \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 20:44:07 2009 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 20:55:47 2009 +0100
     3.3 @@ -52,18 +52,18 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{mldecls}
     3.7 -  \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
     3.8 -  \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
     3.9 -  \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
    3.10 -  \indexml{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
    3.11 -  \indexml{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
    3.12 -  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
    3.13 +  \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
    3.14 +  \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
    3.15 +  \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
    3.16 +  \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
    3.17 +  \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
    3.18 +  \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
    3.19  \verb|    -> theory -> theory| \\
    3.20 -  \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
    3.21 -  \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    3.22 -  \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
    3.23 +  \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
    3.24 +  \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    3.25 +  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
    3.26  \verb|    -> (string * sort) list * (string * typ list) list| \\
    3.27 -  \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
    3.28 +  \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
    3.29    \end{mldecls}
    3.30  
    3.31    \begin{description}
    3.32 @@ -124,9 +124,9 @@
    3.33  %
    3.34  \begin{isamarkuptext}%
    3.35  \begin{mldecls}
    3.36 -  \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
    3.37 -  \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
    3.38 -  \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
    3.39 +  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
    3.40 +  \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
    3.41 +  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
    3.42    \end{mldecls}
    3.43  
    3.44    \begin{description}
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 20:44:07 2009 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 20:55:47 2009 +0100
     4.3 @@ -276,7 +276,7 @@
     4.4  \hspace*{0pt}module Example where {\char123}\\
     4.5  \hspace*{0pt}\\
     4.6  \hspace*{0pt}\\
     4.7 -\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
     4.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
     4.9  \hspace*{0pt}\\
    4.10  \hspace*{0pt}class Semigroup a where {\char123}\\
    4.11  \hspace*{0pt} ~mult ::~a -> a -> a;\\
    4.12 @@ -341,7 +341,7 @@
    4.13  \hspace*{0pt}structure Example = \\
    4.14  \hspace*{0pt}struct\\
    4.15  \hspace*{0pt}\\
    4.16 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    4.17 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    4.18  \hspace*{0pt}\\
    4.19  \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
    4.20  \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
    4.21 @@ -1032,7 +1032,7 @@
    4.22  \hspace*{0pt}structure Example = \\
    4.23  \hspace*{0pt}struct\\
    4.24  \hspace*{0pt}\\
    4.25 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    4.26 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    4.27  \hspace*{0pt}\\
    4.28  \hspace*{0pt}fun null [] = true\\
    4.29  \hspace*{0pt} ~| null (x ::~xs) = false;\\
     5.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 20:44:07 2009 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 20:55:47 2009 +0100
     5.3 @@ -1104,7 +1104,7 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \noindent Clearly, any attempt of a termination proof must fail. And without
     5.7 -  that, we do not get the usual rules \isa{findzero{\isachardot}simp} and 
     5.8 +  that, we do not get the usual rules \isa{findzero{\isachardot}simps} and 
     5.9    \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
    5.10  \end{isamarkuptext}%
    5.11  \isamarkuptrue%
    5.12 @@ -1480,7 +1480,7 @@
    5.13  
    5.14    The predicate \isa{findzero{\isacharunderscore}dom} is the accessible part of
    5.15    that relation. An argument belongs to the accessible part, if it can
    5.16 -  be reached in a finite number of steps (cf.~its definition in \isa{Accessible{\isacharunderscore}Part{\isachardot}thy}).
    5.17 +  be reached in a finite number of steps (cf.~its definition in \isa{Wellfounded{\isachardot}thy}).
    5.18  
    5.19    Since the domain predicate is just an abbreviation, you can use
    5.20    lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some
    5.21 @@ -1823,7 +1823,7 @@
    5.22  As usual, we have to give a wellfounded relation, such that the
    5.23    arguments of the recursive calls get smaller. But what exactly are
    5.24    the arguments of the recursive calls when mirror is given as an
    5.25 -  argument to map? Isabelle gives us the
    5.26 +  argument to \isa{map}? Isabelle gives us the
    5.27    subgoals
    5.28  
    5.29    \begin{isabelle}%
    5.30 @@ -1835,9 +1835,9 @@
    5.31    applies the recursive call \isa{mirror} to elements
    5.32    of \isa{l}, which is essential for the termination proof.
    5.33  
    5.34 -  This knowledge about map is encoded in so-called congruence rules,
    5.35 +  This knowledge about \isa{map} is encoded in so-called congruence rules,
    5.36    which are special theorems known to the \cmd{function} command. The
    5.37 -  rule for map is
    5.38 +  rule for \isa{map} is
    5.39  
    5.40    \begin{isabelle}%
    5.41  {\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys%
     6.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 20:44:07 2009 +0100
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 20:55:47 2009 +0100
     6.3 @@ -81,14 +81,14 @@
     6.4  %
     6.5  \begin{isamarkuptext}%
     6.6  \begin{mldecls}
     6.7 -  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
     6.8 -  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
     6.9 -  \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
    6.10 -  \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
    6.11 -  \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
    6.12 -  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
    6.13 -  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
    6.14 -  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
    6.15 +  \indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\
    6.16 +  \indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
    6.17 +  \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
    6.18 +  \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
    6.19 +  \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
    6.20 +  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
    6.21 +  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
    6.22 +  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
    6.23    \end{mldecls}
    6.24  
    6.25    \begin{description}
    6.26 @@ -171,19 +171,19 @@
    6.27  %
    6.28  \begin{isamarkuptext}%
    6.29  \begin{mldecls}
    6.30 -  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
    6.31 -  \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
    6.32 -  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
    6.33 +  \indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
    6.34 +  \indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
    6.35 +  \indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
    6.36  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.37 -  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
    6.38 +  \indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
    6.39  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.40 -  \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
    6.41 +  \indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
    6.42  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.43 -  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
    6.44 +  \indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
    6.45  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.46 -  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
    6.47 +  \indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
    6.48  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.49 -  \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
    6.50 +  \indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
    6.51  \verb|  Toplevel.transition -> Toplevel.transition| \\
    6.52    \end{mldecls}
    6.53  
    6.54 @@ -300,8 +300,8 @@
    6.55  %
    6.56  \begin{isamarkuptext}%
    6.57  \begin{mldecls}
    6.58 -  \indexml{the\_context}\verb|the_context: unit -> theory| \\
    6.59 -  \indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
    6.60 +  \indexdef{}{ML}{the\_context}\verb|the_context: unit -> theory| \\
    6.61 +  \indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
    6.62    \end{mldecls}
    6.63  
    6.64    \begin{description}
    6.65 @@ -329,12 +329,12 @@
    6.66    \bigskip
    6.67  
    6.68    \begin{mldecls}
    6.69 -  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
    6.70 -  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
    6.71 -  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
    6.72 -  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
    6.73 -  \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
    6.74 -  \indexml{Isar.goal}\verb|Isar.goal: unit -> thm| \\
    6.75 +  \indexdef{}{ML}{Isar.main}\verb|Isar.main: unit -> unit| \\
    6.76 +  \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
    6.77 +  \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
    6.78 +  \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
    6.79 +  \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
    6.80 +  \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
    6.81    \end{mldecls}
    6.82  
    6.83    \begin{description}
    6.84 @@ -434,16 +434,16 @@
    6.85  %
    6.86  \begin{isamarkuptext}%
    6.87  \begin{mldecls}
    6.88 -  \indexml{theory}\verb|theory: string -> theory| \\
    6.89 -  \indexml{use\_thy}\verb|use_thy: string -> unit| \\
    6.90 -  \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
    6.91 -  \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
    6.92 -  \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
    6.93 -  \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
    6.94 -  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
    6.95 -  \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
    6.96 +  \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
    6.97 +  \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
    6.98 +  \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
    6.99 +  \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
   6.100 +  \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
   6.101 +  \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   6.102 +  \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
   6.103 +  \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
   6.104    \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
   6.105 -  \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
   6.106 +  \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
   6.107    \end{mldecls}
   6.108  
   6.109    \begin{description}
     7.1 --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 20:44:07 2009 +0100
     7.2 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 20:55:47 2009 +0100
     7.3 @@ -122,12 +122,12 @@
     7.4  %
     7.5  \begin{isamarkuptext}%
     7.6  \begin{mldecls}
     7.7 -  \indexmltype{local\_theory}\verb|type local_theory = Proof.context| \\
     7.8 -  \indexml{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
     7.9 -  \indexml{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
    7.10 +  \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
    7.11 +  \indexdef{}{ML}{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
    7.12 +  \indexdef{}{ML}{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
    7.13  \verb|    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
    7.14  \verb|    (term * (string * thm)) * local_theory| \\
    7.15 -  \indexml{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
    7.16 +  \indexdef{}{ML}{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
    7.17  \verb|    Attrib.binding * thm list -> local_theory ->|\isasep\isanewline%
    7.18  \verb|    (string * thm list) * local_theory| \\
    7.19    \end{mldecls}
     8.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 20:44:07 2009 +0100
     8.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 20:55:47 2009 +0100
     8.3 @@ -127,22 +127,22 @@
     8.4  %
     8.5  \begin{isamarkuptext}%
     8.6  \begin{mldecls}
     8.7 -  \indexmltype{class}\verb|type class| \\
     8.8 -  \indexmltype{sort}\verb|type sort| \\
     8.9 -  \indexmltype{arity}\verb|type arity| \\
    8.10 -  \indexmltype{typ}\verb|type typ| \\
    8.11 -  \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
    8.12 -  \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
    8.13 +  \indexdef{}{ML type}{class}\verb|type class| \\
    8.14 +  \indexdef{}{ML type}{sort}\verb|type sort| \\
    8.15 +  \indexdef{}{ML type}{arity}\verb|type arity| \\
    8.16 +  \indexdef{}{ML type}{typ}\verb|type typ| \\
    8.17 +  \indexdef{}{ML}{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
    8.18 +  \indexdef{}{ML}{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
    8.19    \end{mldecls}
    8.20    \begin{mldecls}
    8.21 -  \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
    8.22 -  \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
    8.23 -  \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
    8.24 -  \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
    8.25 +  \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
    8.26 +  \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
    8.27 +  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
    8.28 +  \indexdef{}{ML}{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
    8.29  \verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
    8.30 -  \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
    8.31 -  \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    8.32 -  \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    8.33 +  \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
    8.34 +  \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    8.35 +  \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    8.36    \end{mldecls}
    8.37  
    8.38    \begin{description}
    8.39 @@ -314,23 +314,23 @@
    8.40  %
    8.41  \begin{isamarkuptext}%
    8.42  \begin{mldecls}
    8.43 -  \indexmltype{term}\verb|type term| \\
    8.44 -  \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
    8.45 -  \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
    8.46 -  \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
    8.47 -  \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
    8.48 -  \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
    8.49 +  \indexdef{}{ML type}{term}\verb|type term| \\
    8.50 +  \indexdef{}{ML}{op aconv}\verb|op aconv: term * term -> bool| \\
    8.51 +  \indexdef{}{ML}{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
    8.52 +  \indexdef{}{ML}{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
    8.53 +  \indexdef{}{ML}{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
    8.54 +  \indexdef{}{ML}{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
    8.55    \end{mldecls}
    8.56    \begin{mldecls}
    8.57 -  \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
    8.58 -  \indexml{lambda}\verb|lambda: term -> term -> term| \\
    8.59 -  \indexml{betapply}\verb|betapply: term * term -> term| \\
    8.60 -  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
    8.61 +  \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
    8.62 +  \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
    8.63 +  \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
    8.64 +  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
    8.65  \verb|  theory -> term * theory| \\
    8.66 -  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
    8.67 +  \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
    8.68  \verb|  theory -> (term * term) * theory| \\
    8.69 -  \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    8.70 -  \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    8.71 +  \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    8.72 +  \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    8.73    \end{mldecls}
    8.74  
    8.75    \begin{description}
    8.76 @@ -539,29 +539,29 @@
    8.77  %
    8.78  \begin{isamarkuptext}%
    8.79  \begin{mldecls}
    8.80 -  \indexmltype{ctyp}\verb|type ctyp| \\
    8.81 -  \indexmltype{cterm}\verb|type cterm| \\
    8.82 -  \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    8.83 -  \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    8.84 +  \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\
    8.85 +  \indexdef{}{ML type}{cterm}\verb|type cterm| \\
    8.86 +  \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    8.87 +  \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    8.88    \end{mldecls}
    8.89    \begin{mldecls}
    8.90 -  \indexmltype{thm}\verb|type thm| \\
    8.91 -  \indexml{proofs}\verb|proofs: int ref| \\
    8.92 -  \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
    8.93 -  \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
    8.94 -  \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
    8.95 -  \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
    8.96 -  \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
    8.97 -  \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
    8.98 -  \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
    8.99 -  \indexml{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
   8.100 -  \indexml{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
   8.101 +  \indexdef{}{ML type}{thm}\verb|type thm| \\
   8.102 +  \indexdef{}{ML}{proofs}\verb|proofs: int ref| \\
   8.103 +  \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   8.104 +  \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   8.105 +  \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
   8.106 +  \indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
   8.107 +  \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
   8.108 +  \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
   8.109 +  \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
   8.110 +  \indexdef{}{ML}{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
   8.111 +  \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
   8.112  \verb|  -> (string * ('a -> thm)) * theory| \\
   8.113    \end{mldecls}
   8.114    \begin{mldecls}
   8.115 -  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
   8.116 -  \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
   8.117 -  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
   8.118 +  \indexdef{}{ML}{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
   8.119 +  \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
   8.120 +  \indexdef{}{ML}{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
   8.121    \end{mldecls}
   8.122  
   8.123    \begin{description}
   8.124 @@ -697,12 +697,12 @@
   8.125  %
   8.126  \begin{isamarkuptext}%
   8.127  \begin{mldecls}
   8.128 -  \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
   8.129 -  \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
   8.130 -  \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
   8.131 -  \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
   8.132 -  \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
   8.133 -  \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
   8.134 +  \indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
   8.135 +  \indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
   8.136 +  \indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
   8.137 +  \indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
   8.138 +  \indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
   8.139 +  \indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
   8.140    \end{mldecls}
   8.141  
   8.142    \begin{description}
   8.143 @@ -821,7 +821,7 @@
   8.144  %
   8.145  \begin{isamarkuptext}%
   8.146  \begin{mldecls}
   8.147 -  \indexml{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
   8.148 +  \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
   8.149    \end{mldecls}
   8.150  
   8.151    \begin{description}
   8.152 @@ -911,8 +911,8 @@
   8.153  %
   8.154  \begin{isamarkuptext}%
   8.155  \begin{mldecls}
   8.156 -  \indexml{op RS}\verb|op RS: thm * thm -> thm| \\
   8.157 -  \indexml{op OF}\verb|op OF: thm * thm list -> thm| \\
   8.158 +  \indexdef{}{ML}{op RS}\verb|op RS: thm * thm -> thm| \\
   8.159 +  \indexdef{}{ML}{op OF}\verb|op OF: thm * thm list -> thm| \\
   8.160    \end{mldecls}
   8.161  
   8.162    \begin{description}
     9.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 20:44:07 2009 +0100
     9.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 20:55:47 2009 +0100
     9.3 @@ -275,9 +275,9 @@
     9.4  %
     9.5  \begin{isamarkuptext}%
     9.6  \begin{mldecls}
     9.7 -  \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
     9.8 -  \indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
     9.9 -  \indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
    9.10 +  \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
    9.11 +  \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
    9.12 +  \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
    9.13    \end{mldecls}
    9.14  
    9.15    \begin{description}
    9.16 @@ -331,7 +331,7 @@
    9.17  %
    9.18  \begin{isamarkuptext}%
    9.19  \begin{mldecls}
    9.20 -  \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
    9.21 +  \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
    9.22    \end{mldecls}%
    9.23  \end{isamarkuptext}%
    9.24  \isamarkuptrue%
    9.25 @@ -410,10 +410,10 @@
    9.26  %
    9.27  \begin{isamarkuptext}%
    9.28  \begin{mldecls}
    9.29 -  \indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
    9.30 -  \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
    9.31 -  \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
    9.32 -  \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
    9.33 +  \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
    9.34 +  \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
    9.35 +  \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
    9.36 +  \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
    9.37    \end{mldecls}%
    9.38  \end{isamarkuptext}%
    9.39  \isamarkuptrue%
    9.40 @@ -483,8 +483,8 @@
    9.41  %
    9.42  \begin{isamarkuptext}%
    9.43  \begin{mldecls}
    9.44 -  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
    9.45 -  \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    9.46 +  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
    9.47 +  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    9.48    \end{mldecls}%
    9.49  \end{isamarkuptext}%
    9.50  \isamarkuptrue%
    9.51 @@ -545,11 +545,11 @@
    9.52  %
    9.53  \begin{isamarkuptext}%
    9.54  \begin{mldecls}
    9.55 -  \indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
    9.56 -  \indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
    9.57 -  \indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
    9.58 -  \indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
    9.59 -  \indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
    9.60 +  \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
    9.61 +  \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
    9.62 +  \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
    9.63 +  \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
    9.64 +  \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
    9.65    \end{mldecls}%
    9.66  \end{isamarkuptext}%
    9.67  \isamarkuptrue%
    9.68 @@ -576,8 +576,8 @@
    9.69  %
    9.70  \begin{isamarkuptext}%
    9.71  \begin{mldecls}
    9.72 -  \indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
    9.73 -  \indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
    9.74 +  \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
    9.75 +  \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
    9.76    \end{mldecls}%
    9.77  \end{isamarkuptext}%
    9.78  \isamarkuptrue%
    9.79 @@ -619,14 +619,14 @@
    9.80  %
    9.81  \begin{isamarkuptext}%
    9.82  \begin{mldecls}
    9.83 -  \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
    9.84 -  \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
    9.85 -  \indexml{the}\verb|the: 'a option -> 'a| \\
    9.86 -  \indexml{these}\verb|these: 'a list option -> 'a list| \\
    9.87 -  \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
    9.88 -  \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
    9.89 -  \indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
    9.90 -  \indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
    9.91 +  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
    9.92 +  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
    9.93 +  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
    9.94 +  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
    9.95 +  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
    9.96 +  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
    9.97 +  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
    9.98 +  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
    9.99    \end{mldecls}%
   9.100  \end{isamarkuptext}%
   9.101  \isamarkuptrue%
   9.102 @@ -659,10 +659,10 @@
   9.103  %
   9.104  \begin{isamarkuptext}%
   9.105  \begin{mldecls}
   9.106 -  \indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
   9.107 -  \indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
   9.108 -  \indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
   9.109 -  \indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
   9.110 +  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
   9.111 +  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
   9.112 +  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
   9.113 +  \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
   9.114    \end{mldecls}%
   9.115  \end{isamarkuptext}%
   9.116  \isamarkuptrue%
   9.117 @@ -690,19 +690,19 @@
   9.118  %
   9.119  \begin{isamarkuptext}%
   9.120  \begin{mldecls}
   9.121 -  \indexmlexception{AList.DUP}\verb|exception AList.DUP| \\
   9.122 -  \indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
   9.123 -  \indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
   9.124 -  \indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   9.125 -  \indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   9.126 -  \indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
   9.127 -  \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
   9.128 +  \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
   9.129 +  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
   9.130 +  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
   9.131 +  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   9.132 +  \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   9.133 +  \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
   9.134 +  \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
   9.135  \verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
   9.136 -  \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
   9.137 +  \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
   9.138  \verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
   9.139 -  \indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
   9.140 +  \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
   9.141  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
   9.142 -  \indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
   9.143 +  \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
   9.144  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
   9.145    \end{mldecls}%
   9.146  \end{isamarkuptext}%
   9.147 @@ -732,25 +732,25 @@
   9.148  %
   9.149  \begin{isamarkuptext}%
   9.150  \begin{mldecls}
   9.151 -  \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
   9.152 -  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
   9.153 -  \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
   9.154 -  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
   9.155 -  \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   9.156 -  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
   9.157 -  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
   9.158 -  \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   9.159 -  \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
   9.160 -  \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
   9.161 +  \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
   9.162 +  \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
   9.163 +  \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
   9.164 +  \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
   9.165 +  \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   9.166 +  \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
   9.167 +  \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
   9.168 +  \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   9.169 +  \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
   9.170 +  \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
   9.171  \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
   9.172 -  \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
   9.173 +  \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
   9.174  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   9.175 -  \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
   9.176 +  \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
   9.177  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   9.178 -  \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   9.179 +  \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   9.180  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   9.181  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
   9.182 -  \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   9.183 +  \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   9.184  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   9.185  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
   9.186    \end{mldecls}%
    10.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 20:44:07 2009 +0100
    10.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 20:55:47 2009 +0100
    10.3 @@ -170,16 +170,16 @@
    10.4  %
    10.5  \begin{isamarkuptext}%
    10.6  \begin{mldecls}
    10.7 -  \indexmltype{theory}\verb|type theory| \\
    10.8 -  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
    10.9 -  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
   10.10 -  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
   10.11 -  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
   10.12 +  \indexdef{}{ML type}{theory}\verb|type theory| \\
   10.13 +  \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
   10.14 +  \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
   10.15 +  \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
   10.16 +  \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
   10.17    \end{mldecls}
   10.18    \begin{mldecls}
   10.19 -  \indexmltype{theory\_ref}\verb|type theory_ref| \\
   10.20 -  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
   10.21 -  \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   10.22 +  \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
   10.23 +  \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
   10.24 +  \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   10.25    \end{mldecls}
   10.26  
   10.27    \begin{description}
   10.28 @@ -264,10 +264,10 @@
   10.29  %
   10.30  \begin{isamarkuptext}%
   10.31  \begin{mldecls}
   10.32 -  \indexmltype{Proof.context}\verb|type Proof.context| \\
   10.33 -  \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
   10.34 -  \indexml{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
   10.35 -  \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   10.36 +  \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
   10.37 +  \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
   10.38 +  \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
   10.39 +  \indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   10.40    \end{mldecls}
   10.41  
   10.42    \begin{description}
   10.43 @@ -323,9 +323,9 @@
   10.44  %
   10.45  \begin{isamarkuptext}%
   10.46  \begin{mldecls}
   10.47 -  \indexmltype{Context.generic}\verb|type Context.generic| \\
   10.48 -  \indexml{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
   10.49 -  \indexml{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   10.50 +  \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\
   10.51 +  \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
   10.52 +  \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   10.53    \end{mldecls}
   10.54  
   10.55    \begin{description}
   10.56 @@ -435,9 +435,9 @@
   10.57  %
   10.58  \begin{isamarkuptext}%
   10.59  \begin{mldecls}
   10.60 -  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
   10.61 -  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
   10.62 -  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
   10.63 +  \indexdef{}{ML functor}{TheoryDataFun}\verb|functor TheoryDataFun| \\
   10.64 +  \indexdef{}{ML functor}{ProofDataFun}\verb|functor ProofDataFun| \\
   10.65 +  \indexdef{}{ML functor}{GenericDataFun}\verb|functor GenericDataFun| \\
   10.66    \end{mldecls}
   10.67  
   10.68    \begin{description}
   10.69 @@ -537,16 +537,16 @@
   10.70  %
   10.71  \begin{isamarkuptext}%
   10.72  \begin{mldecls}
   10.73 -  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
   10.74 -  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
   10.75 -  \indexml{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   10.76 -  \indexml{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   10.77 -  \indexml{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   10.78 -  \indexml{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   10.79 +  \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol| \\
   10.80 +  \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
   10.81 +  \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   10.82 +  \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   10.83 +  \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   10.84 +  \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   10.85    \end{mldecls}
   10.86    \begin{mldecls}
   10.87 -  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
   10.88 -  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   10.89 +  \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\
   10.90 +  \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   10.91    \end{mldecls}
   10.92  
   10.93    \begin{description}
   10.94 @@ -621,15 +621,15 @@
   10.95  %
   10.96  \begin{isamarkuptext}%
   10.97  \begin{mldecls}
   10.98 -  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
   10.99 -  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
  10.100 +  \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\
  10.101 +  \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\
  10.102    \end{mldecls}
  10.103    \begin{mldecls}
  10.104 -  \indexmltype{Name.context}\verb|type Name.context| \\
  10.105 -  \indexml{Name.context}\verb|Name.context: Name.context| \\
  10.106 -  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
  10.107 -  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
  10.108 -  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
  10.109 +  \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
  10.110 +  \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
  10.111 +  \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
  10.112 +  \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
  10.113 +  \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
  10.114    \end{mldecls}
  10.115  
  10.116    \begin{description}
  10.117 @@ -709,7 +709,7 @@
  10.118  %
  10.119  \begin{isamarkuptext}%
  10.120  \begin{mldecls}
  10.121 -  \indexmltype{indexname}\verb|type indexname| \\
  10.122 +  \indexdef{}{ML type}{indexname}\verb|type indexname| \\
  10.123    \end{mldecls}
  10.124  
  10.125    \begin{description}
  10.126 @@ -791,25 +791,25 @@
  10.127  %
  10.128  \begin{isamarkuptext}%
  10.129  \begin{mldecls}
  10.130 -  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
  10.131 -  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
  10.132 -  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
  10.133 -  \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
  10.134 -  \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
  10.135 +  \indexdef{}{ML}{NameSpace.base}\verb|NameSpace.base: string -> string| \\
  10.136 +  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
  10.137 +  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
  10.138 +  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
  10.139 +  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
  10.140    \end{mldecls}
  10.141    \begin{mldecls}
  10.142 -  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
  10.143 -  \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
  10.144 -  \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
  10.145 -  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
  10.146 +  \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
  10.147 +  \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
  10.148 +  \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
  10.149 +  \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
  10.150    \end{mldecls}
  10.151    \begin{mldecls}
  10.152 -  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
  10.153 -  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
  10.154 -  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
  10.155 -  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
  10.156 -  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
  10.157 -  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
  10.158 +  \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
  10.159 +  \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
  10.160 +  \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
  10.161 +  \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
  10.162 +  \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
  10.163 +  \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
  10.164    \end{mldecls}
  10.165  
  10.166    \begin{description}
    11.1 --- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 20:44:07 2009 +0100
    11.2 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 20:55:47 2009 +0100
    11.3 @@ -103,17 +103,17 @@
    11.4  %
    11.5  \begin{isamarkuptext}%
    11.6  \begin{mldecls}
    11.7 -  \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
    11.8 +  \indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
    11.9  \verb|  string list -> Proof.context -> string list * Proof.context| \\
   11.10 -  \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
   11.11 +  \indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
   11.12  \verb|  string list -> Proof.context -> string list * Proof.context| \\
   11.13 -  \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   11.14 -  \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   11.15 -  \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   11.16 -  \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   11.17 -  \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
   11.18 +  \indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   11.19 +  \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   11.20 +  \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   11.21 +  \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   11.22 +  \indexdef{}{ML}{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
   11.23  \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
   11.24 -  \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   11.25 +  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   11.26    \end{mldecls}
   11.27  
   11.28    \begin{description}
   11.29 @@ -231,13 +231,13 @@
   11.30  %
   11.31  \begin{isamarkuptext}%
   11.32  \begin{mldecls}
   11.33 -  \indexmltype{Assumption.export}\verb|type Assumption.export| \\
   11.34 -  \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
   11.35 -  \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
   11.36 +  \indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\
   11.37 +  \indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
   11.38 +  \indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
   11.39  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
   11.40 -  \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
   11.41 +  \indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
   11.42  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
   11.43 -  \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   11.44 +  \indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   11.45    \end{mldecls}
   11.46  
   11.47    \begin{description}
   11.48 @@ -324,18 +324,18 @@
   11.49  %
   11.50  \begin{isamarkuptext}%
   11.51  \begin{mldecls}
   11.52 -  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
   11.53 +  \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
   11.54  \verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
   11.55  \verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
   11.56    \end{mldecls}
   11.57    \begin{mldecls}
   11.58 -  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
   11.59 +  \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
   11.60  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
   11.61 -  \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
   11.62 +  \indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
   11.63  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
   11.64    \end{mldecls}
   11.65    \begin{mldecls}
   11.66 -  \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
   11.67 +  \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
   11.68  \verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
   11.69    \end{mldecls}
   11.70  
    12.1 --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 20:44:07 2009 +0100
    12.2 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 20:55:47 2009 +0100
    12.3 @@ -83,10 +83,10 @@
    12.4  %
    12.5  \begin{isamarkuptext}%
    12.6  \begin{mldecls}
    12.7 -  \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
    12.8 -  \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
    12.9 -  \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
   12.10 -  \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   12.11 +  \indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
   12.12 +  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: thm -> thm| \\
   12.13 +  \indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
   12.14 +  \indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   12.15    \end{mldecls}
   12.16  
   12.17    \begin{description}
   12.18 @@ -207,13 +207,13 @@
   12.19  %
   12.20  \begin{isamarkuptext}%
   12.21  \begin{mldecls}
   12.22 -  \indexmltype{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
   12.23 -  \indexml{no\_tac}\verb|no_tac: tactic| \\
   12.24 -  \indexml{all\_tac}\verb|all_tac: tactic| \\
   12.25 -  \indexml{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
   12.26 -  \indexml{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
   12.27 -  \indexml{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
   12.28 -  \indexml{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
   12.29 +  \indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
   12.30 +  \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
   12.31 +  \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
   12.32 +  \indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
   12.33 +  \indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
   12.34 +  \indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
   12.35 +  \indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
   12.36    \end{mldecls}
   12.37  
   12.38    \begin{description}
   12.39 @@ -316,15 +316,15 @@
   12.40  %
   12.41  \begin{isamarkuptext}%
   12.42  \begin{mldecls}
   12.43 -  \indexml{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
   12.44 -  \indexml{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
   12.45 -  \indexml{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
   12.46 -  \indexml{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
   12.47 -  \indexml{assume\_tac}\verb|assume_tac: int -> tactic| \\
   12.48 -  \indexml{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
   12.49 -  \indexml{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
   12.50 -  \indexml{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
   12.51 -  \indexml{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
   12.52 +  \indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
   12.53 +  \indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
   12.54 +  \indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
   12.55 +  \indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
   12.56 +  \indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\
   12.57 +  \indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
   12.58 +  \indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
   12.59 +  \indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
   12.60 +  \indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
   12.61    \end{mldecls}
   12.62  
   12.63    \begin{description}
   12.64 @@ -426,11 +426,11 @@
   12.65  %
   12.66  \begin{isamarkuptext}%
   12.67  \begin{mldecls}
   12.68 -  \indexml{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.69 -  \indexml{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.70 -  \indexml{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.71 -  \indexml{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
   12.72 -  \indexml{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
   12.73 +  \indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.74 +  \indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.75 +  \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   12.76 +  \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
   12.77 +  \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
   12.78    \end{mldecls}
   12.79  
   12.80    \begin{description}
    13.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 20:44:07 2009 +0100
    13.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 20:55:47 2009 +0100
    13.3 @@ -118,19 +118,19 @@
    13.4  %
    13.5  \begin{isamarkuptext}%
    13.6  \begin{mldecls} 
    13.7 -    \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
    13.8 -    \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
    13.9 -    \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   13.10 -    \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   13.11 -    \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   13.12 -    \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   13.13 -    \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   13.14 -    \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   13.15 -    \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   13.16 -    \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   13.17 -    \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   13.18 -    \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   13.19 -    \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   13.20 +    \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
   13.21 +    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
   13.22 +    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   13.23 +    \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   13.24 +    \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   13.25 +    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   13.26 +    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   13.27 +    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   13.28 +    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   13.29 +    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   13.30 +    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   13.31 +    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   13.32 +    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   13.33    \end{mldecls}
   13.34  
   13.35    These global ML variables control the detail of information that is
   13.36 @@ -231,9 +231,9 @@
   13.37  %
   13.38  \begin{isamarkuptext}%
   13.39  \begin{mldecls}
   13.40 -    \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   13.41 -    \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   13.42 -    \indexml{print\_depth}\verb|print_depth: int -> unit| \\
   13.43 +    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   13.44 +    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   13.45 +    \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   13.46    \end{mldecls}
   13.47  
   13.48    These ML functions set limits for pretty printed text.
    14.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 20:44:07 2009 +0100
    14.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 20:55:47 2009 +0100
    14.3 @@ -810,8 +810,8 @@
    14.4    \end{matharray}
    14.5  
    14.6    \begin{mldecls}
    14.7 -    \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
    14.8 -    \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
    14.9 +    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   14.10 +    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   14.11    \end{mldecls}
   14.12  
   14.13    \begin{rail}