merged
authorwenzelm
Thu Feb 26 20:57:59 2009 +0100 (2009-02-26)
changeset 3012325a3531c0df5
parent 30117 1cbcebc85914
parent 30122 1c912a9d8200
child 30124 b956bf0dc87c
merged
     1.1 --- a/doc-src/Intro/intro.tex	Thu Feb 26 20:03:58 2009 +0100
     1.2 +++ b/doc-src/Intro/intro.tex	Thu Feb 26 20:57:59 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  %prth *(\(.*\));          \1;      
     1.5  %{\\out \(.*\)}          {\\out val it = "\1" : thm}
     1.6  
     1.7 -\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Introduction to Isabelle}   
     1.8 +\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}   
     1.9  \author{{\em Lawrence C. Paulson}\\
    1.10          Computer Laboratory \\ University of Cambridge \\
    1.11          \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 20:03:58 2009 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 20:57:59 2009 +0100
     2.3 @@ -1153,7 +1153,7 @@
     2.4  \hspace*{0pt}module Example where {\char123}\\
     2.5  \hspace*{0pt}\\
     2.6  \hspace*{0pt}\\
     2.7 -\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
     2.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
     2.9  \hspace*{0pt}\\
    2.10  \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    2.11  \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    2.12 @@ -1240,7 +1240,7 @@
    2.13  \hspace*{0pt}structure Example = \\
    2.14  \hspace*{0pt}struct\\
    2.15  \hspace*{0pt}\\
    2.16 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    2.17 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    2.18  \hspace*{0pt}\\
    2.19  \hspace*{0pt}fun nat{\char95}aux i n =\\
    2.20  \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Thu Feb 26 20:03:58 2009 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Thu Feb 26 20:57:59 2009 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  
     3.5  ML {* no_document use_thys
     3.6    ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
     3.7 -   "~~/src/HOL/Reflection/Ferrack"] *}
     3.8 +   "~~/src/HOL/Decision_Procs/Ferrack"] *}
     3.9  
    3.10  ML_val {* Code_Target.code_width := 74 *}
    3.11  
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 20:03:58 2009 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 20:57:59 2009 +0100
     4.3 @@ -267,9 +267,9 @@
     4.4  \hspace*{0pt}structure Example = \\
     4.5  \hspace*{0pt}struct\\
     4.6  \hspace*{0pt}\\
     4.7 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
     4.8 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
     4.9  \hspace*{0pt}\\
    4.10 -\hspace*{0pt}datatype boola = False | True;\\
    4.11 +\hspace*{0pt}datatype boola = True | False;\\
    4.12  \hspace*{0pt}\\
    4.13  \hspace*{0pt}fun anda x True = x\\
    4.14  \hspace*{0pt} ~| anda x False = False\\
    4.15 @@ -350,7 +350,7 @@
    4.16  \hspace*{0pt}structure Example = \\
    4.17  \hspace*{0pt}struct\\
    4.18  \hspace*{0pt}\\
    4.19 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    4.20 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    4.21  \hspace*{0pt}\\
    4.22  \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    4.23  \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
    4.24 @@ -407,7 +407,7 @@
    4.25  \hspace*{0pt}structure Example = \\
    4.26  \hspace*{0pt}struct\\
    4.27  \hspace*{0pt}\\
    4.28 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    4.29 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    4.30  \hspace*{0pt}\\
    4.31  \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    4.32  \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 20:03:58 2009 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 20:57:59 2009 +0100
     5.3 @@ -52,18 +52,18 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{mldecls}
     5.7 -  \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
     5.8 -  \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
     5.9 -  \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
    5.10 -  \indexml{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
    5.11 -  \indexml{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
    5.12 -  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
    5.13 +  \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
    5.14 +  \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
    5.15 +  \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
    5.16 +  \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
    5.17 +  \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
    5.18 +  \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
    5.19  \verb|    -> theory -> theory| \\
    5.20 -  \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
    5.21 -  \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    5.22 -  \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
    5.23 +  \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
    5.24 +  \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    5.25 +  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
    5.26  \verb|    -> (string * sort) list * (string * typ list) list| \\
    5.27 -  \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
    5.28 +  \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
    5.29    \end{mldecls}
    5.30  
    5.31    \begin{description}
    5.32 @@ -124,9 +124,9 @@
    5.33  %
    5.34  \begin{isamarkuptext}%
    5.35  \begin{mldecls}
    5.36 -  \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
    5.37 -  \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
    5.38 -  \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
    5.39 +  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
    5.40 +  \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
    5.41 +  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
    5.42    \end{mldecls}
    5.43  
    5.44    \begin{description}
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 20:03:58 2009 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 20:57:59 2009 +0100
     6.3 @@ -276,7 +276,7 @@
     6.4  \hspace*{0pt}module Example where {\char123}\\
     6.5  \hspace*{0pt}\\
     6.6  \hspace*{0pt}\\
     6.7 -\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
     6.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
     6.9  \hspace*{0pt}\\
    6.10  \hspace*{0pt}class Semigroup a where {\char123}\\
    6.11  \hspace*{0pt} ~mult ::~a -> a -> a;\\
    6.12 @@ -341,7 +341,7 @@
    6.13  \hspace*{0pt}structure Example = \\
    6.14  \hspace*{0pt}struct\\
    6.15  \hspace*{0pt}\\
    6.16 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    6.17 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    6.18  \hspace*{0pt}\\
    6.19  \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
    6.20  \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
    6.21 @@ -1032,7 +1032,7 @@
    6.22  \hspace*{0pt}structure Example = \\
    6.23  \hspace*{0pt}struct\\
    6.24  \hspace*{0pt}\\
    6.25 -\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    6.26 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
    6.27  \hspace*{0pt}\\
    6.28  \hspace*{0pt}fun null [] = true\\
    6.29  \hspace*{0pt} ~| null (x ::~xs) = false;\\
     7.1 --- a/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:03:58 2009 +0100
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:57:59 2009 +0100
     7.3 @@ -6,12 +6,6 @@
     7.4  %% references
     7.5  \newcommand{\secref}[1]{\S\ref{#1}}
     7.6  
     7.7 -%% index
     7.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     7.9 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    7.10 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    7.11 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    7.12 -
    7.13  %% logical markup
    7.14  \newcommand{\strong}[1]{{\bfseries {#1}}}
    7.15  \newcommand{\qn}[1]{\emph{#1}}
     8.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 20:03:58 2009 +0100
     8.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 20:57:59 2009 +0100
     8.3 @@ -1104,7 +1104,7 @@
     8.4  %
     8.5  \begin{isamarkuptext}%
     8.6  \noindent Clearly, any attempt of a termination proof must fail. And without
     8.7 -  that, we do not get the usual rules \isa{findzero{\isachardot}simp} and 
     8.8 +  that, we do not get the usual rules \isa{findzero{\isachardot}simps} and 
     8.9    \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
    8.10  \end{isamarkuptext}%
    8.11  \isamarkuptrue%
    8.12 @@ -1480,7 +1480,7 @@
    8.13  
    8.14    The predicate \isa{findzero{\isacharunderscore}dom} is the accessible part of
    8.15    that relation. An argument belongs to the accessible part, if it can
    8.16 -  be reached in a finite number of steps (cf.~its definition in \isa{Accessible{\isacharunderscore}Part{\isachardot}thy}).
    8.17 +  be reached in a finite number of steps (cf.~its definition in \isa{Wellfounded{\isachardot}thy}).
    8.18  
    8.19    Since the domain predicate is just an abbreviation, you can use
    8.20    lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some
    8.21 @@ -1823,7 +1823,7 @@
    8.22  As usual, we have to give a wellfounded relation, such that the
    8.23    arguments of the recursive calls get smaller. But what exactly are
    8.24    the arguments of the recursive calls when mirror is given as an
    8.25 -  argument to map? Isabelle gives us the
    8.26 +  argument to \isa{map}? Isabelle gives us the
    8.27    subgoals
    8.28  
    8.29    \begin{isabelle}%
    8.30 @@ -1835,9 +1835,9 @@
    8.31    applies the recursive call \isa{mirror} to elements
    8.32    of \isa{l}, which is essential for the termination proof.
    8.33  
    8.34 -  This knowledge about map is encoded in so-called congruence rules,
    8.35 +  This knowledge about \isa{map} is encoded in so-called congruence rules,
    8.36    which are special theorems known to the \cmd{function} command. The
    8.37 -  rule for map is
    8.38 +  rule for \isa{map} is
    8.39  
    8.40    \begin{isabelle}%
    8.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%
     9.1 --- a/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:03:58 2009 +0100
     9.2 +++ b/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:57:59 2009 +0100
     9.3 @@ -7,12 +7,6 @@
     9.4  \newcommand{\chref}[1]{chapter~\ref{#1}}
     9.5  \newcommand{\figref}[1]{figure~\ref{#1}}
     9.6  
     9.7 -%% index
     9.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     9.9 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    9.10 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    9.11 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    9.12 -
    9.13  %% math
    9.14  \newcommand{\text}[1]{\mbox{#1}}
    9.15  \newcommand{\isasymvartheta}{\isamath{\theta}}
    10.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 20:03:58 2009 +0100
    10.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 20:57:59 2009 +0100
    10.3 @@ -81,14 +81,14 @@
    10.4  %
    10.5  \begin{isamarkuptext}%
    10.6  \begin{mldecls}
    10.7 -  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
    10.8 -  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
    10.9 -  \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
   10.10 -  \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
   10.11 -  \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
   10.12 -  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
   10.13 -  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
   10.14 -  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
   10.15 +  \indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\
   10.16 +  \indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
   10.17 +  \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
   10.18 +  \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
   10.19 +  \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
   10.20 +  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
   10.21 +  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
   10.22 +  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
   10.23    \end{mldecls}
   10.24  
   10.25    \begin{description}
   10.26 @@ -171,19 +171,19 @@
   10.27  %
   10.28  \begin{isamarkuptext}%
   10.29  \begin{mldecls}
   10.30 -  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
   10.31 -  \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
   10.32 -  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
   10.33 +  \indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
   10.34 +  \indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
   10.35 +  \indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
   10.36  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.37 -  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
   10.38 +  \indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
   10.39  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.40 -  \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
   10.41 +  \indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
   10.42  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.43 -  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
   10.44 +  \indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
   10.45  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.46 -  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
   10.47 +  \indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
   10.48  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.49 -  \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
   10.50 +  \indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
   10.51  \verb|  Toplevel.transition -> Toplevel.transition| \\
   10.52    \end{mldecls}
   10.53  
   10.54 @@ -300,8 +300,8 @@
   10.55  %
   10.56  \begin{isamarkuptext}%
   10.57  \begin{mldecls}
   10.58 -  \indexml{the\_context}\verb|the_context: unit -> theory| \\
   10.59 -  \indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
   10.60 +  \indexdef{}{ML}{the\_context}\verb|the_context: unit -> theory| \\
   10.61 +  \indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
   10.62    \end{mldecls}
   10.63  
   10.64    \begin{description}
   10.65 @@ -329,12 +329,12 @@
   10.66    \bigskip
   10.67  
   10.68    \begin{mldecls}
   10.69 -  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
   10.70 -  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
   10.71 -  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
   10.72 -  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
   10.73 -  \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
   10.74 -  \indexml{Isar.goal}\verb|Isar.goal: unit -> thm| \\
   10.75 +  \indexdef{}{ML}{Isar.main}\verb|Isar.main: unit -> unit| \\
   10.76 +  \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
   10.77 +  \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
   10.78 +  \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
   10.79 +  \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
   10.80 +  \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
   10.81    \end{mldecls}
   10.82  
   10.83    \begin{description}
   10.84 @@ -434,16 +434,16 @@
   10.85  %
   10.86  \begin{isamarkuptext}%
   10.87  \begin{mldecls}
   10.88 -  \indexml{theory}\verb|theory: string -> theory| \\
   10.89 -  \indexml{use\_thy}\verb|use_thy: string -> unit| \\
   10.90 -  \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
   10.91 -  \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
   10.92 -  \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
   10.93 -  \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   10.94 -  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
   10.95 -  \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
   10.96 +  \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
   10.97 +  \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
   10.98 +  \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
   10.99 +  \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
  10.100 +  \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
  10.101 +  \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
  10.102 +  \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
  10.103 +  \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
  10.104    \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
  10.105 -  \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
  10.106 +  \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
  10.107    \end{mldecls}
  10.108  
  10.109    \begin{description}
    11.1 --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 20:03:58 2009 +0100
    11.2 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 20:57:59 2009 +0100
    11.3 @@ -122,12 +122,12 @@
    11.4  %
    11.5  \begin{isamarkuptext}%
    11.6  \begin{mldecls}
    11.7 -  \indexmltype{local\_theory}\verb|type local_theory = Proof.context| \\
    11.8 -  \indexml{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
    11.9 -  \indexml{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
   11.10 +  \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
   11.11 +  \indexdef{}{ML}{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
   11.12 +  \indexdef{}{ML}{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
   11.13  \verb|    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
   11.14  \verb|    (term * (string * thm)) * local_theory| \\
   11.15 -  \indexml{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
   11.16 +  \indexdef{}{ML}{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
   11.17  \verb|    Attrib.binding * thm list -> local_theory ->|\isasep\isanewline%
   11.18  \verb|    (string * thm list) * local_theory| \\
   11.19    \end{mldecls}
    12.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 20:03:58 2009 +0100
    12.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 20:57:59 2009 +0100
    12.3 @@ -127,22 +127,22 @@
    12.4  %
    12.5  \begin{isamarkuptext}%
    12.6  \begin{mldecls}
    12.7 -  \indexmltype{class}\verb|type class| \\
    12.8 -  \indexmltype{sort}\verb|type sort| \\
    12.9 -  \indexmltype{arity}\verb|type arity| \\
   12.10 -  \indexmltype{typ}\verb|type typ| \\
   12.11 -  \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
   12.12 -  \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
   12.13 +  \indexdef{}{ML type}{class}\verb|type class| \\
   12.14 +  \indexdef{}{ML type}{sort}\verb|type sort| \\
   12.15 +  \indexdef{}{ML type}{arity}\verb|type arity| \\
   12.16 +  \indexdef{}{ML type}{typ}\verb|type typ| \\
   12.17 +  \indexdef{}{ML}{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
   12.18 +  \indexdef{}{ML}{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
   12.19    \end{mldecls}
   12.20    \begin{mldecls}
   12.21 -  \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   12.22 -  \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
   12.23 -  \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
   12.24 -  \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
   12.25 +  \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   12.26 +  \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
   12.27 +  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
   12.28 +  \indexdef{}{ML}{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
   12.29  \verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
   12.30 -  \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
   12.31 -  \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
   12.32 -  \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
   12.33 +  \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
   12.34 +  \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
   12.35 +  \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
   12.36    \end{mldecls}
   12.37  
   12.38    \begin{description}
   12.39 @@ -314,23 +314,23 @@
   12.40  %
   12.41  \begin{isamarkuptext}%
   12.42  \begin{mldecls}
   12.43 -  \indexmltype{term}\verb|type term| \\
   12.44 -  \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
   12.45 -  \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
   12.46 -  \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
   12.47 -  \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
   12.48 -  \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
   12.49 +  \indexdef{}{ML type}{term}\verb|type term| \\
   12.50 +  \indexdef{}{ML}{op aconv}\verb|op aconv: term * term -> bool| \\
   12.51 +  \indexdef{}{ML}{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
   12.52 +  \indexdef{}{ML}{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
   12.53 +  \indexdef{}{ML}{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
   12.54 +  \indexdef{}{ML}{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
   12.55    \end{mldecls}
   12.56    \begin{mldecls}
   12.57 -  \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
   12.58 -  \indexml{lambda}\verb|lambda: term -> term -> term| \\
   12.59 -  \indexml{betapply}\verb|betapply: term * term -> term| \\
   12.60 -  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
   12.61 +  \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
   12.62 +  \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
   12.63 +  \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
   12.64 +  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
   12.65  \verb|  theory -> term * theory| \\
   12.66 -  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
   12.67 +  \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
   12.68  \verb|  theory -> (term * term) * theory| \\
   12.69 -  \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   12.70 -  \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   12.71 +  \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   12.72 +  \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   12.73    \end{mldecls}
   12.74  
   12.75    \begin{description}
   12.76 @@ -539,29 +539,29 @@
   12.77  %
   12.78  \begin{isamarkuptext}%
   12.79  \begin{mldecls}
   12.80 -  \indexmltype{ctyp}\verb|type ctyp| \\
   12.81 -  \indexmltype{cterm}\verb|type cterm| \\
   12.82 -  \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
   12.83 -  \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
   12.84 +  \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\
   12.85 +  \indexdef{}{ML type}{cterm}\verb|type cterm| \\
   12.86 +  \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
   12.87 +  \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
   12.88    \end{mldecls}
   12.89    \begin{mldecls}
   12.90 -  \indexmltype{thm}\verb|type thm| \\
   12.91 -  \indexml{proofs}\verb|proofs: int ref| \\
   12.92 -  \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   12.93 -  \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   12.94 -  \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
   12.95 -  \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
   12.96 -  \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
   12.97 -  \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
   12.98 -  \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
   12.99 -  \indexml{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
  12.100 -  \indexml{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
  12.101 +  \indexdef{}{ML type}{thm}\verb|type thm| \\
  12.102 +  \indexdef{}{ML}{proofs}\verb|proofs: int ref| \\
  12.103 +  \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
  12.104 +  \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
  12.105 +  \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
  12.106 +  \indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
  12.107 +  \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
  12.108 +  \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
  12.109 +  \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
  12.110 +  \indexdef{}{ML}{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
  12.111 +  \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
  12.112  \verb|  -> (string * ('a -> thm)) * theory| \\
  12.113    \end{mldecls}
  12.114    \begin{mldecls}
  12.115 -  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
  12.116 -  \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
  12.117 -  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
  12.118 +  \indexdef{}{ML}{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
  12.119 +  \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
  12.120 +  \indexdef{}{ML}{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
  12.121    \end{mldecls}
  12.122  
  12.123    \begin{description}
  12.124 @@ -697,12 +697,12 @@
  12.125  %
  12.126  \begin{isamarkuptext}%
  12.127  \begin{mldecls}
  12.128 -  \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
  12.129 -  \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
  12.130 -  \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
  12.131 -  \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
  12.132 -  \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
  12.133 -  \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
  12.134 +  \indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
  12.135 +  \indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
  12.136 +  \indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
  12.137 +  \indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
  12.138 +  \indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
  12.139 +  \indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
  12.140    \end{mldecls}
  12.141  
  12.142    \begin{description}
  12.143 @@ -821,7 +821,7 @@
  12.144  %
  12.145  \begin{isamarkuptext}%
  12.146  \begin{mldecls}
  12.147 -  \indexml{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
  12.148 +  \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
  12.149    \end{mldecls}
  12.150  
  12.151    \begin{description}
  12.152 @@ -911,8 +911,8 @@
  12.153  %
  12.154  \begin{isamarkuptext}%
  12.155  \begin{mldecls}
  12.156 -  \indexml{op RS}\verb|op RS: thm * thm -> thm| \\
  12.157 -  \indexml{op OF}\verb|op OF: thm * thm list -> thm| \\
  12.158 +  \indexdef{}{ML}{op RS}\verb|op RS: thm * thm -> thm| \\
  12.159 +  \indexdef{}{ML}{op OF}\verb|op OF: thm * thm list -> thm| \\
  12.160    \end{mldecls}
  12.161  
  12.162    \begin{description}
    13.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 20:03:58 2009 +0100
    13.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 20:57:59 2009 +0100
    13.3 @@ -275,9 +275,9 @@
    13.4  %
    13.5  \begin{isamarkuptext}%
    13.6  \begin{mldecls}
    13.7 -  \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
    13.8 -  \indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
    13.9 -  \indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
   13.10 +  \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
   13.11 +  \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
   13.12 +  \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
   13.13    \end{mldecls}
   13.14  
   13.15    \begin{description}
   13.16 @@ -331,7 +331,7 @@
   13.17  %
   13.18  \begin{isamarkuptext}%
   13.19  \begin{mldecls}
   13.20 -  \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
   13.21 +  \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
   13.22    \end{mldecls}%
   13.23  \end{isamarkuptext}%
   13.24  \isamarkuptrue%
   13.25 @@ -410,10 +410,10 @@
   13.26  %
   13.27  \begin{isamarkuptext}%
   13.28  \begin{mldecls}
   13.29 -  \indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
   13.30 -  \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
   13.31 -  \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
   13.32 -  \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
   13.33 +  \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
   13.34 +  \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
   13.35 +  \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
   13.36 +  \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
   13.37    \end{mldecls}%
   13.38  \end{isamarkuptext}%
   13.39  \isamarkuptrue%
   13.40 @@ -483,8 +483,8 @@
   13.41  %
   13.42  \begin{isamarkuptext}%
   13.43  \begin{mldecls}
   13.44 -  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
   13.45 -  \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
   13.46 +  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
   13.47 +  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
   13.48    \end{mldecls}%
   13.49  \end{isamarkuptext}%
   13.50  \isamarkuptrue%
   13.51 @@ -545,11 +545,11 @@
   13.52  %
   13.53  \begin{isamarkuptext}%
   13.54  \begin{mldecls}
   13.55 -  \indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
   13.56 -  \indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
   13.57 -  \indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
   13.58 -  \indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
   13.59 -  \indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
   13.60 +  \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
   13.61 +  \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
   13.62 +  \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
   13.63 +  \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
   13.64 +  \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
   13.65    \end{mldecls}%
   13.66  \end{isamarkuptext}%
   13.67  \isamarkuptrue%
   13.68 @@ -576,8 +576,8 @@
   13.69  %
   13.70  \begin{isamarkuptext}%
   13.71  \begin{mldecls}
   13.72 -  \indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
   13.73 -  \indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
   13.74 +  \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
   13.75 +  \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
   13.76    \end{mldecls}%
   13.77  \end{isamarkuptext}%
   13.78  \isamarkuptrue%
   13.79 @@ -619,14 +619,14 @@
   13.80  %
   13.81  \begin{isamarkuptext}%
   13.82  \begin{mldecls}
   13.83 -  \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
   13.84 -  \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
   13.85 -  \indexml{the}\verb|the: 'a option -> 'a| \\
   13.86 -  \indexml{these}\verb|these: 'a list option -> 'a list| \\
   13.87 -  \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
   13.88 -  \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
   13.89 -  \indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
   13.90 -  \indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
   13.91 +  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
   13.92 +  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
   13.93 +  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
   13.94 +  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
   13.95 +  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
   13.96 +  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
   13.97 +  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
   13.98 +  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
   13.99    \end{mldecls}%
  13.100  \end{isamarkuptext}%
  13.101  \isamarkuptrue%
  13.102 @@ -659,10 +659,10 @@
  13.103  %
  13.104  \begin{isamarkuptext}%
  13.105  \begin{mldecls}
  13.106 -  \indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
  13.107 -  \indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
  13.108 -  \indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
  13.109 -  \indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
  13.110 +  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
  13.111 +  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
  13.112 +  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
  13.113 +  \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
  13.114    \end{mldecls}%
  13.115  \end{isamarkuptext}%
  13.116  \isamarkuptrue%
  13.117 @@ -690,19 +690,19 @@
  13.118  %
  13.119  \begin{isamarkuptext}%
  13.120  \begin{mldecls}
  13.121 -  \indexmlexception{AList.DUP}\verb|exception AList.DUP| \\
  13.122 -  \indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
  13.123 -  \indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
  13.124 -  \indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
  13.125 -  \indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
  13.126 -  \indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
  13.127 -  \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
  13.128 +  \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
  13.129 +  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
  13.130 +  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
  13.131 +  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
  13.132 +  \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
  13.133 +  \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
  13.134 +  \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
  13.135  \verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
  13.136 -  \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
  13.137 +  \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
  13.138  \verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
  13.139 -  \indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
  13.140 +  \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
  13.141  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
  13.142 -  \indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
  13.143 +  \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
  13.144  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
  13.145    \end{mldecls}%
  13.146  \end{isamarkuptext}%
  13.147 @@ -732,25 +732,25 @@
  13.148  %
  13.149  \begin{isamarkuptext}%
  13.150  \begin{mldecls}
  13.151 -  \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
  13.152 -  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
  13.153 -  \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
  13.154 -  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
  13.155 -  \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
  13.156 -  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
  13.157 -  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
  13.158 -  \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
  13.159 -  \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
  13.160 -  \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
  13.161 +  \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
  13.162 +  \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
  13.163 +  \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
  13.164 +  \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
  13.165 +  \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
  13.166 +  \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
  13.167 +  \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
  13.168 +  \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
  13.169 +  \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
  13.170 +  \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
  13.171  \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
  13.172 -  \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
  13.173 +  \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
  13.174  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
  13.175 -  \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
  13.176 +  \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
  13.177  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
  13.178 -  \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
  13.179 +  \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
  13.180  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
  13.181  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
  13.182 -  \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
  13.183 +  \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
  13.184  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
  13.185  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
  13.186    \end{mldecls}%
    14.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 20:03:58 2009 +0100
    14.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 20:57:59 2009 +0100
    14.3 @@ -170,16 +170,16 @@
    14.4  %
    14.5  \begin{isamarkuptext}%
    14.6  \begin{mldecls}
    14.7 -  \indexmltype{theory}\verb|type theory| \\
    14.8 -  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
    14.9 -  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
   14.10 -  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
   14.11 -  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
   14.12 +  \indexdef{}{ML type}{theory}\verb|type theory| \\
   14.13 +  \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
   14.14 +  \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
   14.15 +  \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
   14.16 +  \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
   14.17    \end{mldecls}
   14.18    \begin{mldecls}
   14.19 -  \indexmltype{theory\_ref}\verb|type theory_ref| \\
   14.20 -  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
   14.21 -  \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   14.22 +  \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
   14.23 +  \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
   14.24 +  \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   14.25    \end{mldecls}
   14.26  
   14.27    \begin{description}
   14.28 @@ -264,10 +264,10 @@
   14.29  %
   14.30  \begin{isamarkuptext}%
   14.31  \begin{mldecls}
   14.32 -  \indexmltype{Proof.context}\verb|type Proof.context| \\
   14.33 -  \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
   14.34 -  \indexml{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
   14.35 -  \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   14.36 +  \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
   14.37 +  \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
   14.38 +  \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
   14.39 +  \indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   14.40    \end{mldecls}
   14.41  
   14.42    \begin{description}
   14.43 @@ -323,9 +323,9 @@
   14.44  %
   14.45  \begin{isamarkuptext}%
   14.46  \begin{mldecls}
   14.47 -  \indexmltype{Context.generic}\verb|type Context.generic| \\
   14.48 -  \indexml{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
   14.49 -  \indexml{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   14.50 +  \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\
   14.51 +  \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
   14.52 +  \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   14.53    \end{mldecls}
   14.54  
   14.55    \begin{description}
   14.56 @@ -435,9 +435,9 @@
   14.57  %
   14.58  \begin{isamarkuptext}%
   14.59  \begin{mldecls}
   14.60 -  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
   14.61 -  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
   14.62 -  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
   14.63 +  \indexdef{}{ML functor}{TheoryDataFun}\verb|functor TheoryDataFun| \\
   14.64 +  \indexdef{}{ML functor}{ProofDataFun}\verb|functor ProofDataFun| \\
   14.65 +  \indexdef{}{ML functor}{GenericDataFun}\verb|functor GenericDataFun| \\
   14.66    \end{mldecls}
   14.67  
   14.68    \begin{description}
   14.69 @@ -537,16 +537,16 @@
   14.70  %
   14.71  \begin{isamarkuptext}%
   14.72  \begin{mldecls}
   14.73 -  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
   14.74 -  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
   14.75 -  \indexml{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   14.76 -  \indexml{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   14.77 -  \indexml{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   14.78 -  \indexml{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   14.79 +  \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol| \\
   14.80 +  \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
   14.81 +  \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   14.82 +  \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   14.83 +  \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   14.84 +  \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   14.85    \end{mldecls}
   14.86    \begin{mldecls}
   14.87 -  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
   14.88 -  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   14.89 +  \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\
   14.90 +  \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   14.91    \end{mldecls}
   14.92  
   14.93    \begin{description}
   14.94 @@ -621,15 +621,15 @@
   14.95  %
   14.96  \begin{isamarkuptext}%
   14.97  \begin{mldecls}
   14.98 -  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
   14.99 -  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
  14.100 +  \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\
  14.101 +  \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\
  14.102    \end{mldecls}
  14.103    \begin{mldecls}
  14.104 -  \indexmltype{Name.context}\verb|type Name.context| \\
  14.105 -  \indexml{Name.context}\verb|Name.context: Name.context| \\
  14.106 -  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
  14.107 -  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
  14.108 -  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
  14.109 +  \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
  14.110 +  \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
  14.111 +  \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
  14.112 +  \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
  14.113 +  \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
  14.114    \end{mldecls}
  14.115  
  14.116    \begin{description}
  14.117 @@ -709,7 +709,7 @@
  14.118  %
  14.119  \begin{isamarkuptext}%
  14.120  \begin{mldecls}
  14.121 -  \indexmltype{indexname}\verb|type indexname| \\
  14.122 +  \indexdef{}{ML type}{indexname}\verb|type indexname| \\
  14.123    \end{mldecls}
  14.124  
  14.125    \begin{description}
  14.126 @@ -791,25 +791,25 @@
  14.127  %
  14.128  \begin{isamarkuptext}%
  14.129  \begin{mldecls}
  14.130 -  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
  14.131 -  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
  14.132 -  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
  14.133 -  \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
  14.134 -  \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
  14.135 +  \indexdef{}{ML}{NameSpace.base}\verb|NameSpace.base: string -> string| \\
  14.136 +  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
  14.137 +  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
  14.138 +  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
  14.139 +  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
  14.140    \end{mldecls}
  14.141    \begin{mldecls}
  14.142 -  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
  14.143 -  \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
  14.144 -  \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
  14.145 -  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
  14.146 +  \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
  14.147 +  \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
  14.148 +  \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
  14.149 +  \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
  14.150    \end{mldecls}
  14.151    \begin{mldecls}
  14.152 -  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
  14.153 -  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
  14.154 -  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
  14.155 -  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
  14.156 -  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
  14.157 -  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
  14.158 +  \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
  14.159 +  \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
  14.160 +  \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
  14.161 +  \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
  14.162 +  \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
  14.163 +  \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
  14.164    \end{mldecls}
  14.165  
  14.166    \begin{description}
    15.1 --- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 20:03:58 2009 +0100
    15.2 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 20:57:59 2009 +0100
    15.3 @@ -103,17 +103,17 @@
    15.4  %
    15.5  \begin{isamarkuptext}%
    15.6  \begin{mldecls}
    15.7 -  \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
    15.8 +  \indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
    15.9  \verb|  string list -> Proof.context -> string list * Proof.context| \\
   15.10 -  \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
   15.11 +  \indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
   15.12  \verb|  string list -> Proof.context -> string list * Proof.context| \\
   15.13 -  \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   15.14 -  \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   15.15 -  \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   15.16 -  \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   15.17 -  \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
   15.18 +  \indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   15.19 +  \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   15.20 +  \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   15.21 +  \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   15.22 +  \indexdef{}{ML}{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
   15.23  \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
   15.24 -  \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   15.25 +  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   15.26    \end{mldecls}
   15.27  
   15.28    \begin{description}
   15.29 @@ -231,13 +231,13 @@
   15.30  %
   15.31  \begin{isamarkuptext}%
   15.32  \begin{mldecls}
   15.33 -  \indexmltype{Assumption.export}\verb|type Assumption.export| \\
   15.34 -  \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
   15.35 -  \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
   15.36 +  \indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\
   15.37 +  \indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
   15.38 +  \indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
   15.39  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
   15.40 -  \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
   15.41 +  \indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
   15.42  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
   15.43 -  \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   15.44 +  \indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   15.45    \end{mldecls}
   15.46  
   15.47    \begin{description}
   15.48 @@ -324,18 +324,18 @@
   15.49  %
   15.50  \begin{isamarkuptext}%
   15.51  \begin{mldecls}
   15.52 -  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
   15.53 +  \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
   15.54  \verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
   15.55  \verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
   15.56    \end{mldecls}
   15.57    \begin{mldecls}
   15.58 -  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
   15.59 +  \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
   15.60  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
   15.61 -  \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
   15.62 +  \indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
   15.63  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
   15.64    \end{mldecls}
   15.65    \begin{mldecls}
   15.66 -  \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
   15.67 +  \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
   15.68  \verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
   15.69    \end{mldecls}
   15.70  
    16.1 --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 20:03:58 2009 +0100
    16.2 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 20:57:59 2009 +0100
    16.3 @@ -83,10 +83,10 @@
    16.4  %
    16.5  \begin{isamarkuptext}%
    16.6  \begin{mldecls}
    16.7 -  \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
    16.8 -  \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
    16.9 -  \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
   16.10 -  \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   16.11 +  \indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
   16.12 +  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: thm -> thm| \\
   16.13 +  \indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
   16.14 +  \indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   16.15    \end{mldecls}
   16.16  
   16.17    \begin{description}
   16.18 @@ -207,13 +207,13 @@
   16.19  %
   16.20  \begin{isamarkuptext}%
   16.21  \begin{mldecls}
   16.22 -  \indexmltype{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
   16.23 -  \indexml{no\_tac}\verb|no_tac: tactic| \\
   16.24 -  \indexml{all\_tac}\verb|all_tac: tactic| \\
   16.25 -  \indexml{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
   16.26 -  \indexml{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
   16.27 -  \indexml{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
   16.28 -  \indexml{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
   16.29 +  \indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
   16.30 +  \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
   16.31 +  \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
   16.32 +  \indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
   16.33 +  \indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
   16.34 +  \indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
   16.35 +  \indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
   16.36    \end{mldecls}
   16.37  
   16.38    \begin{description}
   16.39 @@ -316,15 +316,15 @@
   16.40  %
   16.41  \begin{isamarkuptext}%
   16.42  \begin{mldecls}
   16.43 -  \indexml{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
   16.44 -  \indexml{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
   16.45 -  \indexml{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
   16.46 -  \indexml{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
   16.47 -  \indexml{assume\_tac}\verb|assume_tac: int -> tactic| \\
   16.48 -  \indexml{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
   16.49 -  \indexml{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
   16.50 -  \indexml{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
   16.51 -  \indexml{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
   16.52 +  \indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
   16.53 +  \indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
   16.54 +  \indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
   16.55 +  \indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
   16.56 +  \indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\
   16.57 +  \indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
   16.58 +  \indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
   16.59 +  \indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
   16.60 +  \indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
   16.61    \end{mldecls}
   16.62  
   16.63    \begin{description}
   16.64 @@ -426,11 +426,11 @@
   16.65  %
   16.66  \begin{isamarkuptext}%
   16.67  \begin{mldecls}
   16.68 -  \indexml{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.69 -  \indexml{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.70 -  \indexml{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.71 -  \indexml{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
   16.72 -  \indexml{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
   16.73 +  \indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.74 +  \indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.75 +  \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
   16.76 +  \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
   16.77 +  \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
   16.78    \end{mldecls}
   16.79  
   16.80    \begin{description}
    17.1 --- a/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:03:58 2009 +0100
    17.2 +++ b/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:57:59 2009 +0100
    17.3 @@ -7,13 +7,6 @@
    17.4  \newcommand{\chref}[1]{chapter~\ref{#1}}
    17.5  \newcommand{\figref}[1]{figure~\ref{#1}}
    17.6  
    17.7 -%% index
    17.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    17.9 -\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
   17.10 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
   17.11 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
   17.12 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
   17.13 -
   17.14  %% math
   17.15  \newcommand{\text}[1]{\mbox{#1}}
   17.16  \newcommand{\isasymvartheta}{\isamath{\theta}}
    18.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 20:03:58 2009 +0100
    18.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 20:57:59 2009 +0100
    18.3 @@ -118,19 +118,19 @@
    18.4  %
    18.5  \begin{isamarkuptext}%
    18.6  \begin{mldecls} 
    18.7 -    \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
    18.8 -    \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
    18.9 -    \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   18.10 -    \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   18.11 -    \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   18.12 -    \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   18.13 -    \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   18.14 -    \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   18.15 -    \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   18.16 -    \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   18.17 -    \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   18.18 -    \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   18.19 -    \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   18.20 +    \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
   18.21 +    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
   18.22 +    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   18.23 +    \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   18.24 +    \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   18.25 +    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   18.26 +    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   18.27 +    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   18.28 +    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   18.29 +    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   18.30 +    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   18.31 +    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   18.32 +    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   18.33    \end{mldecls}
   18.34  
   18.35    These global ML variables control the detail of information that is
   18.36 @@ -231,9 +231,9 @@
   18.37  %
   18.38  \begin{isamarkuptext}%
   18.39  \begin{mldecls}
   18.40 -    \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   18.41 -    \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   18.42 -    \indexml{print\_depth}\verb|print_depth: int -> unit| \\
   18.43 +    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   18.44 +    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   18.45 +    \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   18.46    \end{mldecls}
   18.47  
   18.48    These ML functions set limits for pretty printed text.
    19.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 20:03:58 2009 +0100
    19.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 20:57:59 2009 +0100
    19.3 @@ -810,8 +810,8 @@
    19.4    \end{matharray}
    19.5  
    19.6    \begin{mldecls}
    19.7 -    \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
    19.8 -    \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
    19.9 +    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   19.10 +    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   19.11    \end{mldecls}
   19.12  
   19.13    \begin{rail}
    20.1 --- a/doc-src/IsarRef/style.sty	Thu Feb 26 20:03:58 2009 +0100
    20.2 +++ b/doc-src/IsarRef/style.sty	Thu Feb 26 20:57:59 2009 +0100
    20.3 @@ -15,7 +15,6 @@
    20.4  
    20.5  %% ML
    20.6  \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
    20.7 -\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
    20.8  
    20.9  %% Isar
   20.10  \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
    21.1 --- a/doc-src/Ref/ref.tex	Thu Feb 26 20:03:58 2009 +0100
    21.2 +++ b/doc-src/Ref/ref.tex	Thu Feb 26 20:57:59 2009 +0100
    21.3 @@ -7,7 +7,7 @@
    21.4  %%% to delete old ones:  \\indexbold{\*[^}]*}
    21.5  %% run    sedindex ref    to prepare index file
    21.6  %%% needs chapter on Provers/typedsimp.ML?
    21.7 -\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}
    21.8 +\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
    21.9  
   21.10  \author{{\em Lawrence C. Paulson}\\
   21.11          Computer Laboratory \\ University of Cambridge \\
    22.1 --- a/doc-src/antiquote_setup.ML	Thu Feb 26 20:03:58 2009 +0100
    22.2 +++ b/doc-src/antiquote_setup.ML	Thu Feb 26 20:57:59 2009 +0100
    22.3 @@ -16,10 +16,11 @@
    22.4  
    22.5  val clean_string = translate
    22.6    (fn "_" => "\\_"
    22.7 +    | "#" => "\\#"
    22.8      | "<" => "$<$"
    22.9      | ">" => "$>$"
   22.10 -    | "#" => "\\#"
   22.11      | "{" => "\\{"
   22.12 +    | "|" => "$\\mid$"
   22.13      | "}" => "\\}"
   22.14      | "\\<dash>" => "-"
   22.15      | c => c);
   22.16 @@ -68,8 +69,9 @@
   22.17      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
   22.18      val _ = writeln (ml (txt1, txt2));
   22.19      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
   22.20 +    val kind' = if kind = "" then "ML" else "ML " ^ kind;
   22.21    in
   22.22 -    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
   22.23 +    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
   22.24      (txt'
   22.25      |> (if ! O.quotes then quote else I)
   22.26      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    23.1 --- a/doc/Contents	Thu Feb 26 20:03:58 2009 +0100
    23.2 +++ b/doc/Contents	Thu Feb 26 20:57:59 2009 +0100
    23.3 @@ -13,8 +13,8 @@
    23.4    system          The Isabelle System Manual
    23.5  
    23.6  Old Manuals (outdated!)
    23.7 -  intro           Introduction to Isabelle
    23.8 -  ref             The Isabelle Reference Manual
    23.9 +  intro           Old Introduction to Isabelle
   23.10 +  ref             Old Isabelle Reference Manual
   23.11    logics          Isabelle's Logics: overview and misc logics
   23.12    logics-HOL      Isabelle's Logics: HOL
   23.13    logics-ZF       Isabelle's Logics: FOL and ZF
    24.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:03:58 2009 +0100
    24.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:57:59 2009 +0100
    24.3 @@ -1,7 +1,9 @@
    24.4 -(* Title:     HOL/Reflection/Approximation.thy
    24.5 - * Author:    Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009
    24.6 - *)
    24.7 +(*  Title:      HOL/Reflection/Approximation.thy
    24.8 +    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
    24.9 +*)
   24.10 +
   24.11  header {* Prove unequations about real numbers by computation *}
   24.12 +
   24.13  theory Approximation
   24.14  imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
   24.15  begin
    25.1 --- a/src/HOL/Library/Float.thy	Thu Feb 26 20:03:58 2009 +0100
    25.2 +++ b/src/HOL/Library/Float.thy	Thu Feb 26 20:57:59 2009 +0100
    25.3 @@ -1,7 +1,7 @@
    25.4 -(* Title:    HOL/Library/Float.thy
    25.5 - * Author:   Steven Obua 2008
    25.6 - *           Johannes H\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
    25.7 - *)
    25.8 +(*  Title:      HOL/Library/Float.thy
    25.9 +    Author:     Steven Obua 2008
   25.10 +    Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
   25.11 +*)
   25.12  
   25.13  header {* Floating-Point Numbers *}
   25.14  
    26.1 --- a/src/HOL/RComplete.thy	Thu Feb 26 20:03:58 2009 +0100
    26.2 +++ b/src/HOL/RComplete.thy	Thu Feb 26 20:57:59 2009 +0100
    26.3 @@ -1,8 +1,8 @@
    26.4 -(*  Title       : HOL/RComplete.thy
    26.5 -    Author      : Jacques D. Fleuriot, University of Edinburgh
    26.6 -    Author      : Larry Paulson, University of Cambridge
    26.7 -    Author      : Jeremy Avigad, Carnegie Mellon University
    26.8 -    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
    26.9 +(*  Title:      HOL/RComplete.thy
   26.10 +    Author:     Jacques D. Fleuriot, University of Edinburgh
   26.11 +    Author:     Larry Paulson, University of Cambridge
   26.12 +    Author:     Jeremy Avigad, Carnegie Mellon University
   26.13 +    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
   26.14  *)
   26.15  
   26.16  header {* Completeness of the Reals; Floor and Ceiling Functions *}
    27.1 --- a/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:03:58 2009 +0100
    27.2 +++ b/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:57:59 2009 +0100
    27.3 @@ -1,6 +1,7 @@
    27.4 -(* Title:    HOL/ex/ApproximationEx.thy
    27.5 -   Author:   Johannes Hoelzl <hoelzl@in.tum.de> 2009
    27.6 +(*  Title:      HOL/ex/ApproximationEx.thy
    27.7 +    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
    27.8  *)
    27.9 +
   27.10  theory ApproximationEx
   27.11  imports "~~/src/HOL/Reflection/Approximation"
   27.12  begin