# HG changeset patch
# User huffman
# Date 1235690838 28800
# Node ID 258f9adfdda543dd81f79974b7b2b582f4087847
# Parent  243a05a67c4167eb1ddafb0f42f92c924c15f539# Parent  cd3f37ba3e2530a1ee5ad39a29acd84d4b67ce8f
merged

diff -r 243a05a67c41 -r 258f9adfdda5 Admin/isatest/settings/sun-poly
--- a/Admin/isatest/settings/sun-poly	Thu Feb 26 11:17:38 2009 -0800
+++ b/Admin/isatest/settings/sun-poly	Thu Feb 26 15:27:18 2009 -0800
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-5.1"
   ML_PLATFORM="sparc-solaris"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1500"
+  ML_OPTIONS="-H 1000"
 
 ISABELLE_HOME_USER=/tmp/isabelle-sun-poly
 
diff -r 243a05a67c41 -r 258f9adfdda5 Admin/makedist
--- a/Admin/makedist	Thu Feb 26 11:17:38 2009 -0800
+++ b/Admin/makedist	Thu Feb 26 15:27:18 2009 -0800
@@ -4,7 +4,7 @@
 
 ## global settings
 
-REPOS="https://isabelle.in.tum.de/repos/isabelle"
+REPOS="http://isabelle.in.tum.de/repos/isabelle"
 
 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/Intro/intro.tex
--- a/doc-src/Intro/intro.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/Intro/intro.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -7,7 +7,7 @@
 %prth *(\(.*\));          \1;      
 %{\\out \(.*\)}          {\\out val it = "\1" : thm}
 
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Introduction to Isabelle}   
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}   
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -1153,7 +1153,7 @@
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
 \hspace*{0pt}\\
-\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
@@ -1240,7 +1240,7 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun nat{\char95}aux i n =\\
 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -5,7 +5,7 @@
 
 ML {* no_document use_thys
   ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
-   "~~/src/HOL/Reflection/Ferrack"] *}
+   "~~/src/HOL/Decision_Procs/Ferrack"] *}
 
 ML_val {* Code_Target.code_width := 74 *}
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -267,9 +267,9 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype boola = False | True;\\
+\hspace*{0pt}datatype boola = True | False;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun anda x True = x\\
 \hspace*{0pt} ~| anda x False = False\\
@@ -350,7 +350,7 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
@@ -407,7 +407,7 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -52,18 +52,18 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
-  \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
-  \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
-  \indexml{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
-  \indexml{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
-  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+  \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
+  \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
+  \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
+  \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
+  \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
+  \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
 \verb|    -> theory -> theory| \\
-  \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
-  \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
-  \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+  \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
+  \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
+  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
 \verb|    -> (string * sort) list * (string * typ list) list| \\
-  \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+  \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
   \end{mldecls}
 
   \begin{description}
@@ -124,9 +124,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
-  \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
-  \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
+  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
+  \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
+  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -276,7 +276,7 @@
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
 \hspace*{0pt}\\
-\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}class Semigroup a where {\char123}\\
 \hspace*{0pt} ~mult ::~a -> a -> a;\\
@@ -341,7 +341,7 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
@@ -1032,7 +1032,7 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun null [] = true\\
 \hspace*{0pt} ~| null (x ::~xs) = false;\\
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Codegen/style.sty
--- a/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 15:27:18 2009 -0800
@@ -6,12 +6,6 @@
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
-
 %% logical markup
 \newcommand{\strong}[1]{{\bfseries {#1}}}
 \newcommand{\qn}[1]{\emph{#1}}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -1104,7 +1104,7 @@
 %
 \begin{isamarkuptext}%
 \noindent Clearly, any attempt of a termination proof must fail. And without
-  that, we do not get the usual rules \isa{findzero{\isachardot}simp} and 
+  that, we do not get the usual rules \isa{findzero{\isachardot}simps} and 
   \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -1480,7 +1480,7 @@
 
   The predicate \isa{findzero{\isacharunderscore}dom} is the accessible part of
   that relation. An argument belongs to the accessible part, if it can
-  be reached in a finite number of steps (cf.~its definition in \isa{Accessible{\isacharunderscore}Part{\isachardot}thy}).
+  be reached in a finite number of steps (cf.~its definition in \isa{Wellfounded{\isachardot}thy}).
 
   Since the domain predicate is just an abbreviation, you can use
   lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some
@@ -1823,7 +1823,7 @@
 As usual, we have to give a wellfounded relation, such that the
   arguments of the recursive calls get smaller. But what exactly are
   the arguments of the recursive calls when mirror is given as an
-  argument to map? Isabelle gives us the
+  argument to \isa{map}? Isabelle gives us the
   subgoals
 
   \begin{isabelle}%
@@ -1835,9 +1835,9 @@
   applies the recursive call \isa{mirror} to elements
   of \isa{l}, which is essential for the termination proof.
 
-  This knowledge about map is encoded in so-called congruence rules,
+  This knowledge about \isa{map} is encoded in so-called congruence rules,
   which are special theorems known to the \cmd{function} command. The
-  rule for map is
+  rule for \isa{map} is
 
   \begin{isabelle}%
 {\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%
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarAdvanced/Functions/style.sty
--- a/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 15:27:18 2009 -0800
@@ -7,12 +7,6 @@
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
-
 %% math
 \newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/IsaMakefile
--- a/doc-src/IsarImplementation/IsaMakefile	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/IsaMakefile	Thu Feb 26 15:27:18 2009 -0800
@@ -23,7 +23,8 @@
 
 $(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy	\
   Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy	\
-  Thy/Proof.thy Thy/Tactic.thy Thy/ML.thy ../antiquote_setup.ML
+  Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy		\
+  ../antiquote_setup.ML
 	@$(USEDIR) Pure Thy
 
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Makefile
--- a/doc-src/IsarImplementation/Makefile	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Makefile	Thu Feb 26 15:27:18 2009 -0800
@@ -10,12 +10,12 @@
 
 NAME = implementation
 
-FILES = implementation.tex Thy/document/Prelim.tex			\
-  Thy/document/Logic.tex Thy/document/Tactic.tex			\
-  Thy/document/Proof.tex Thy/document/Local_Theory.tex			\
-  Thy/document/Integration.tex style.sty ../iman.sty ../extra.sty	\
-  ../isar.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty	\
-  ../manual.bib ../proof.sty
+FILES = ../extra.sty ../iman.sty ../isabelle.sty ../isabellesym.sty	\
+  ../isar.sty ../manual.bib ../pdfsetup.sty ../proof.sty		\
+  Thy/document/Integration.tex Thy/document/Local_Theory.tex		\
+  Thy/document/Logic.tex Thy/document/Prelim.tex			\
+  Thy/document/Proof.tex Thy/document/Syntax.tex			\
+  Thy/document/Tactic.tex implementation.tex style.sty
 
 dvi: $(NAME).dvi
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/ROOT.ML
--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Thu Feb 26 15:27:18 2009 -0800
@@ -1,8 +1,11 @@
-use_thy "Prelim";
-use_thy "Logic";
-use_thy "Tactic";
-use_thy "Proof";
-use_thy "Isar";
-use_thy "Local_Theory";
-use_thy "Integration";
-use_thy "ML";
+use_thys [
+  "Integration",
+  "Isar",
+  "Local_Theory",
+  "Logic",
+  "ML",
+  "Prelim",
+  "Proof",
+  "Syntax",
+  "Tactic"
+];
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/Syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -0,0 +1,9 @@
+theory Syntax
+imports Base
+begin
+
+chapter {* Syntax and type-checking *}
+
+text FIXME
+
+end
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -81,14 +81,14 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
-  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
-  \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
-  \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
-  \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
-  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
-  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
-  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
+  \indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\
+  \indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
+  \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
+  \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
+  \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
+  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
+  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
+  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
   \end{mldecls}
 
   \begin{description}
@@ -171,19 +171,19 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
+  \indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
+  \indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \end{mldecls}
 
@@ -300,8 +300,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{the\_context}\verb|the_context: unit -> theory| \\
-  \indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
+  \indexdef{}{ML}{the\_context}\verb|the_context: unit -> theory| \\
+  \indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
   \end{mldecls}
 
   \begin{description}
@@ -329,12 +329,12 @@
   \bigskip
 
   \begin{mldecls}
-  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
-  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
-  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
-  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
-  \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
-  \indexml{Isar.goal}\verb|Isar.goal: unit -> thm| \\
+  \indexdef{}{ML}{Isar.main}\verb|Isar.main: unit -> unit| \\
+  \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
+  \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
+  \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
+  \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
+  \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -434,16 +434,16 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{theory}\verb|theory: string -> theory| \\
-  \indexml{use\_thy}\verb|use_thy: string -> unit| \\
-  \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
-  \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
-  \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
-  \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
-  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
-  \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
+  \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
+  \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
+  \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
+  \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
+  \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
+  \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
+  \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
+  \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
   \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
-  \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
+  \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
   \end{mldecls}
 
   \begin{description}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -122,12 +122,12 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{local\_theory}\verb|type local_theory = Proof.context| \\
-  \indexml{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
-  \indexml{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
+  \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
+  \indexdef{}{ML}{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
+  \indexdef{}{ML}{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
 \verb|    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
 \verb|    (term * (string * thm)) * local_theory| \\
-  \indexml{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
+  \indexdef{}{ML}{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
 \verb|    Attrib.binding * thm list -> local_theory ->|\isasep\isanewline%
 \verb|    (string * thm list) * local_theory| \\
   \end{mldecls}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -127,22 +127,22 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{class}\verb|type class| \\
-  \indexmltype{sort}\verb|type sort| \\
-  \indexmltype{arity}\verb|type arity| \\
-  \indexmltype{typ}\verb|type typ| \\
-  \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
-  \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
+  \indexdef{}{ML type}{class}\verb|type class| \\
+  \indexdef{}{ML type}{sort}\verb|type sort| \\
+  \indexdef{}{ML type}{arity}\verb|type arity| \\
+  \indexdef{}{ML type}{typ}\verb|type typ| \\
+  \indexdef{}{ML}{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
+  \indexdef{}{ML}{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
-  \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
-  \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
-  \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
+  \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
+  \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
+  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
 \verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
-  \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
-  \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
-  \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
   \end{mldecls}
 
   \begin{description}
@@ -314,23 +314,23 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{term}\verb|type term| \\
-  \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
-  \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
-  \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
-  \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
-  \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
+  \indexdef{}{ML type}{term}\verb|type term| \\
+  \indexdef{}{ML}{op aconv}\verb|op aconv: term * term -> bool| \\
+  \indexdef{}{ML}{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
+  \indexdef{}{ML}{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
+  \indexdef{}{ML}{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
+  \indexdef{}{ML}{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
-  \indexml{lambda}\verb|lambda: term -> term -> term| \\
-  \indexml{betapply}\verb|betapply: term * term -> term| \\
-  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
+  \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
+  \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
+  \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
+  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
 \verb|  theory -> term * theory| \\
-  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
+  \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
 \verb|  theory -> (term * term) * theory| \\
-  \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
-  \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
+  \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
+  \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   \end{mldecls}
 
   \begin{description}
@@ -539,29 +539,29 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{ctyp}\verb|type ctyp| \\
-  \indexmltype{cterm}\verb|type cterm| \\
-  \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
-  \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
+  \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\
+  \indexdef{}{ML type}{cterm}\verb|type cterm| \\
+  \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
+  \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{thm}\verb|type thm| \\
-  \indexml{proofs}\verb|proofs: int ref| \\
-  \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
-  \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
-  \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
-  \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
-  \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
-  \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
-  \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
-  \indexml{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
-  \indexml{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
+  \indexdef{}{ML type}{thm}\verb|type thm| \\
+  \indexdef{}{ML}{proofs}\verb|proofs: int ref| \\
+  \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
+  \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
+  \indexdef{}{ML}{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
+  \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
 \verb|  -> (string * ('a -> thm)) * theory| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
-  \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
-  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
+  \indexdef{}{ML}{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
+  \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
+  \indexdef{}{ML}{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
   \end{mldecls}
 
   \begin{description}
@@ -697,12 +697,12 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
-  \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
-  \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
-  \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
-  \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
-  \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
+  \indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
+  \indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
+  \indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
+  \indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
+  \indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
+  \indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
   \end{mldecls}
 
   \begin{description}
@@ -821,7 +821,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
+  \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -911,8 +911,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{op RS}\verb|op RS: thm * thm -> thm| \\
-  \indexml{op OF}\verb|op OF: thm * thm list -> thm| \\
+  \indexdef{}{ML}{op RS}\verb|op RS: thm * thm -> thm| \\
+  \indexdef{}{ML}{op OF}\verb|op OF: thm * thm list -> thm| \\
   \end{mldecls}
 
   \begin{description}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -275,9 +275,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
-  \indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
-  \indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+  \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
+  \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
+  \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
   \end{mldecls}
 
   \begin{description}
@@ -331,7 +331,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
+  \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -410,10 +410,10 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
-  \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
-  \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
-  \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
+  \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
+  \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
+  \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
+  \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -483,8 +483,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
-  \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
+  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
+  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -545,11 +545,11 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
-  \indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
-  \indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
-  \indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
-  \indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
+  \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
+  \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
+  \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
+  \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
+  \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -576,8 +576,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
-  \indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
+  \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
+  \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -619,14 +619,14 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
-  \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
-  \indexml{the}\verb|the: 'a option -> 'a| \\
-  \indexml{these}\verb|these: 'a list option -> 'a list| \\
-  \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
-  \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
-  \indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
-  \indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
+  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
+  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
+  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
+  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
+  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
+  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
+  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
+  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -659,10 +659,10 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
-  \indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
-  \indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
-  \indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
+  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
+  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
+  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
+  \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -690,19 +690,19 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmlexception{AList.DUP}\verb|exception AList.DUP| \\
-  \indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
-  \indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
-  \indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
-  \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
+  \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
+  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
+  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
+  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
+  \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
+  \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
+  \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
 \verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
-  \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
+  \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
 \verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
+  \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
 \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
-  \indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
+  \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
 \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
   \end{mldecls}%
 \end{isamarkuptext}%
@@ -732,25 +732,25 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
-  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
-  \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
-  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
-  \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
-  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
-  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
-  \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
+  \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
+  \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
+  \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
+  \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
+  \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
+  \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
+  \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
+  \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
+  \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
 \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
-  \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
+  \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
+  \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
+  \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
 \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
-  \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
+  \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
 \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
   \end{mldecls}%
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -170,16 +170,16 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{theory}\verb|type theory| \\
-  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
-  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
-  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
-  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
+  \indexdef{}{ML type}{theory}\verb|type theory| \\
+  \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
+  \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
+  \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
+  \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{theory\_ref}\verb|type theory_ref| \\
-  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
-  \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
+  \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
+  \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
+  \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   \end{mldecls}
 
   \begin{description}
@@ -264,10 +264,10 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{Proof.context}\verb|type Proof.context| \\
-  \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
-  \indexml{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
-  \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
+  \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
+  \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
+  \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
+  \indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -323,9 +323,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{Context.generic}\verb|type Context.generic| \\
-  \indexml{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
-  \indexml{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
+  \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\
+  \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
+  \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -435,9 +435,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
-  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
-  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
+  \indexdef{}{ML functor}{TheoryDataFun}\verb|functor TheoryDataFun| \\
+  \indexdef{}{ML functor}{ProofDataFun}\verb|functor ProofDataFun| \\
+  \indexdef{}{ML functor}{GenericDataFun}\verb|functor GenericDataFun| \\
   \end{mldecls}
 
   \begin{description}
@@ -537,16 +537,16 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
-  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
-  \indexml{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
-  \indexml{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
-  \indexml{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
-  \indexml{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+  \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol| \\
+  \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
+  \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
+  \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
+  \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
+  \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
-  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
+  \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\
+  \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   \end{mldecls}
 
   \begin{description}
@@ -621,15 +621,15 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
-  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
+  \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\
+  \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{Name.context}\verb|type Name.context| \\
-  \indexml{Name.context}\verb|Name.context: Name.context| \\
-  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
-  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
-  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
+  \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
+  \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
+  \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
+  \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
+  \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -709,7 +709,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{indexname}\verb|type indexname| \\
+  \indexdef{}{ML type}{indexname}\verb|type indexname| \\
   \end{mldecls}
 
   \begin{description}
@@ -791,25 +791,25 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
-  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
-  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
-  \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
-  \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
+  \indexdef{}{ML}{NameSpace.base}\verb|NameSpace.base: string -> string| \\
+  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
+  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
+  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
+  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
-  \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
-  \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
-  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
+  \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
+  \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
+  \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
+  \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
-  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
-  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
-  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
-  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
-  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
+  \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
+  \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
+  \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
+  \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
+  \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
+  \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   \end{mldecls}
 
   \begin{description}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Proof.tex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -103,17 +103,17 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
+  \indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
-  \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
+  \indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
-  \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
-  \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
-  \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
-  \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
-  \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+  \indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
+  \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
+  \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
+  \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
+  \indexdef{}{ML}{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
 \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
-  \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
+  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -231,13 +231,13 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{Assumption.export}\verb|type Assumption.export| \\
-  \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
-  \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
+  \indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\
+  \indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
+  \indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
 \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
-  \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
+  \indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
 \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
-  \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
+  \indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -324,18 +324,18 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
+  \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
 \verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
 \verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
+  \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
 \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
-  \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
+  \indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
 \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
+  \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
 \verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
   \end{mldecls}
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Syntax.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -0,0 +1,48 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Syntax}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Syntax\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Syntax and type-checking%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -83,10 +83,10 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
-  \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
-  \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
-  \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
+  \indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
+  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: thm -> thm| \\
+  \indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
+  \indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
@@ -207,13 +207,13 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexmltype{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
-  \indexml{no\_tac}\verb|no_tac: tactic| \\
-  \indexml{all\_tac}\verb|all_tac: tactic| \\
-  \indexml{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
-  \indexml{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
-  \indexml{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
-  \indexml{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
+  \indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
+  \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
+  \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
+  \indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
+  \indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
+  \indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
+  \indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
   \end{mldecls}
 
   \begin{description}
@@ -316,15 +316,15 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
-  \indexml{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
-  \indexml{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
-  \indexml{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
-  \indexml{assume\_tac}\verb|assume_tac: int -> tactic| \\
-  \indexml{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
-  \indexml{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
-  \indexml{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
-  \indexml{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
+  \indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\
+  \indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
+  \indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
   \end{mldecls}
 
   \begin{description}
@@ -426,11 +426,11 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
-  \indexml{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
-  \indexml{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
-  \indexml{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
-  \indexml{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
+  \indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
+  \indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
+  \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
+  \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
+  \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
   \end{mldecls}
 
   \begin{description}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/Thy/document/session.tex
--- a/doc-src/IsarImplementation/Thy/document/session.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/session.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -1,21 +1,23 @@
 \input{Base.tex}
 
-\input{Prelim.tex}
-
-\input{Logic.tex}
-
-\input{Tactic.tex}
-
-\input{Proof.tex}
+\input{Integration.tex}
 
 \input{Isar.tex}
 
 \input{Local_Theory.tex}
 
-\input{Integration.tex}
+\input{Logic.tex}
 
 \input{ML.tex}
 
+\input{Prelim.tex}
+
+\input{Proof.tex}
+
+\input{Syntax.tex}
+
+\input{Tactic.tex}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/implementation.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -69,6 +69,7 @@
 \input{Thy/document/Logic.tex}
 \input{Thy/document/Tactic.tex}
 \input{Thy/document/Proof.tex}
+\input{Thy/document/Syntax.tex}
 \input{Thy/document/Isar.tex}
 \input{Thy/document/Local_Theory.tex}
 \input{Thy/document/Integration.tex}
@@ -78,7 +79,7 @@
 
 \begingroup
 \tocentry{\bibname}
-\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliographystyle{abbrv} \small\raggedright\frenchspacing
 \bibliography{../manual}
 \endgroup
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarImplementation/style.sty	Thu Feb 26 15:27:18 2009 -0800
@@ -7,13 +7,6 @@
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
-
 %% math
 \newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -118,19 +118,19 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls} 
-    \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
-    \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
-    \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
-    \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
-    \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
-    \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
-    \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
-    \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
-    \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
-    \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
-    \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
-    \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
-    \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
+    \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
+    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
+    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
+    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is
@@ -231,9 +231,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-    \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
-    \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
-    \indexml{print\_depth}\verb|print_depth: int -> unit| \\
+    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
+    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
+    \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   \end{mldecls}
 
   These ML functions set limits for pretty printed text.
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -810,8 +810,8 @@
   \end{matharray}
 
   \begin{mldecls}
-    \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
-    \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
+    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
+    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   \end{mldecls}
 
   \begin{rail}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarRef/isar-ref.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -104,7 +104,7 @@
 \input{Thy/document/ML_Tactic.tex}
 
 \begingroup
-  \bibliographystyle{plain} \small\raggedright\frenchspacing
+  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
   \bibliography{../manual}
 \endgroup
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/IsarRef/style.sty	Thu Feb 26 15:27:18 2009 -0800
@@ -15,7 +15,6 @@
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
-\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/Ref/ref.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -7,7 +7,7 @@
 %%% to delete old ones:  \\indexbold{\*[^}]*}
 %% run    sedindex ref    to prepare index file
 %%% needs chapter on Provers/typedsimp.ML?
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
 
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/System/system.tex
--- a/doc-src/System/system.tex	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/System/system.tex	Thu Feb 26 15:27:18 2009 -0800
@@ -36,7 +36,7 @@
 \input{Thy/document/Misc.tex}
 
 \begingroup
-  \bibliographystyle{plain} \small\raggedright\frenchspacing
+  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
   \bibliography{../manual}
 \endgroup
 
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/antiquote_setup.ML	Thu Feb 26 15:27:18 2009 -0800
@@ -16,10 +16,11 @@
 
 val clean_string = translate
   (fn "_" => "\\_"
+    | "#" => "\\#"
     | "<" => "$<$"
     | ">" => "$>$"
-    | "#" => "\\#"
     | "{" => "\\{"
+    | "|" => "$\\mid$"
     | "}" => "\\}"
     | "\\<dash>" => "-"
     | c => c);
@@ -68,8 +69,9 @@
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     val _ = writeln (ml (txt1, txt2));
     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+    val kind' = if kind = "" then "ML" else "ML " ^ kind;
   in
-    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
+    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
     (txt'
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
diff -r 243a05a67c41 -r 258f9adfdda5 doc-src/manual.bib
--- a/doc-src/manual.bib	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc-src/manual.bib	Thu Feb 26 15:27:18 2009 -0800
@@ -467,6 +467,17 @@
   number        = {364/07}
 }
 
+@InProceedings{Haftmann-Wenzel:2009,
+  author        = {Florian Haftmann and Makarius Wenzel},
+  title         = {Local theory specifications in {Isabelle/Isar}},
+  editor        = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
+  booktitle     = {Types for Proofs and Programs, TYPES 2008},
+  publisher     = {Springer},
+  series        = {LNCS},
+  volume        = {????},
+  year          = {2009}
+}
+
 @manual{isabelle-classes,
   author        = {Florian Haftmann},
   title         = {Haskell-style type classes with {Isabelle}/{Isar}},
diff -r 243a05a67c41 -r 258f9adfdda5 doc/Contents
--- a/doc/Contents	Thu Feb 26 11:17:38 2009 -0800
+++ b/doc/Contents	Thu Feb 26 15:27:18 2009 -0800
@@ -13,8 +13,8 @@
   system          The Isabelle System Manual
 
 Old Manuals (outdated!)
-  intro           Introduction to Isabelle
-  ref             The Isabelle Reference Manual
+  intro           Old Introduction to Isabelle
+  ref             Old Isabelle Reference Manual
   logics          Isabelle's Logics: overview and misc logics
   logics-HOL      Isabelle's Logics: HOL
   logics-ZF       Isabelle's Logics: FOL and ZF
diff -r 243a05a67c41 -r 258f9adfdda5 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 11:17:38 2009 -0800
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -1,7 +1,9 @@
-(* Title:     HOL/Reflection/Approximation.thy
- * Author:    Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009
- *)
+(*  Title:      HOL/Reflection/Approximation.thy
+    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
+*)
+
 header {* Prove unequations about real numbers by computation *}
+
 theory Approximation
 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
 begin
diff -r 243a05a67c41 -r 258f9adfdda5 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Feb 26 11:17:38 2009 -0800
+++ b/src/HOL/Library/Float.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -1,7 +1,7 @@
-(* Title:    HOL/Library/Float.thy
- * Author:   Steven Obua 2008
- *           Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
- *)
+(*  Title:      HOL/Library/Float.thy
+    Author:     Steven Obua 2008
+    Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
+*)
 
 header {* Floating-Point Numbers *}
 
diff -r 243a05a67c41 -r 258f9adfdda5 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Thu Feb 26 11:17:38 2009 -0800
+++ b/src/HOL/RComplete.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -1,8 +1,8 @@
-(*  Title       : HOL/RComplete.thy
-    Author      : Jacques D. Fleuriot, University of Edinburgh
-    Author      : Larry Paulson, University of Cambridge
-    Author      : Jeremy Avigad, Carnegie Mellon University
-    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
+(*  Title:      HOL/RComplete.thy
+    Author:     Jacques D. Fleuriot, University of Edinburgh
+    Author:     Larry Paulson, University of Cambridge
+    Author:     Jeremy Avigad, Carnegie Mellon University
+    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
 *)
 
 header {* Completeness of the Reals; Floor and Ceiling Functions *}
diff -r 243a05a67c41 -r 258f9adfdda5 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Feb 26 11:17:38 2009 -0800
+++ b/src/HOL/ROOT.ML	Thu Feb 26 15:27:18 2009 -0800
@@ -1,7 +1,5 @@
 (* Classical Higher-order Logic -- batteries included *)
 
-use_thy "Main";
-share_common_data ();
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
diff -r 243a05a67c41 -r 258f9adfdda5 src/HOL/ex/ApproximationEx.thy
--- a/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 11:17:38 2009 -0800
+++ b/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 15:27:18 2009 -0800
@@ -1,6 +1,7 @@
-(* Title:    HOL/ex/ApproximationEx.thy
-   Author:   Johannes Hoelzl <hoelzl@in.tum.de> 2009
+(*  Title:      HOL/ex/ApproximationEx.thy
+    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
 *)
+
 theory ApproximationEx
 imports "~~/src/HOL/Reflection/Approximation"
 begin