--- a/doc-src/Intro/intro.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/Intro/intro.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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]
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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\\
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Thu Feb 26 20:57:59 2009 +0100
@@ -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 *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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\\
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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;\\
--- a/doc-src/IsarAdvanced/Codegen/style.sty Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty Thu Feb 26 20:57:59 2009 +0100
@@ -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}}
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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%
--- a/doc-src/IsarAdvanced/Functions/style.sty Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/style.sty Thu Feb 26 20:57:59 2009 +0100
@@ -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}}
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}%
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarImplementation/style.sty Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarImplementation/style.sty Thu Feb 26 20:57:59 2009 +0100
@@ -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}}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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.
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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}
--- a/doc-src/IsarRef/style.sty Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/IsarRef/style.sty Thu Feb 26 20:57:59 2009 +0100
@@ -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}\,}}
--- a/doc-src/Ref/ref.tex Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/Ref/ref.tex Thu Feb 26 20:57:59 2009 +0100
@@ -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 \\
--- a/doc-src/antiquote_setup.ML Thu Feb 26 20:03:58 2009 +0100
+++ b/doc-src/antiquote_setup.ML Thu Feb 26 20:57:59 2009 +0100
@@ -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}"
--- a/doc/Contents Thu Feb 26 20:03:58 2009 +0100
+++ b/doc/Contents Thu Feb 26 20:57:59 2009 +0100
@@ -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
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Feb 26 20:03:58 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Feb 26 20:57:59 2009 +0100
@@ -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
--- a/src/HOL/Library/Float.thy Thu Feb 26 20:03:58 2009 +0100
+++ b/src/HOL/Library/Float.thy Thu Feb 26 20:57:59 2009 +0100
@@ -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 *}
--- a/src/HOL/RComplete.thy Thu Feb 26 20:03:58 2009 +0100
+++ b/src/HOL/RComplete.thy Thu Feb 26 20:57:59 2009 +0100
@@ -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 *}
--- a/src/HOL/ex/ApproximationEx.thy Thu Feb 26 20:03:58 2009 +0100
+++ b/src/HOL/ex/ApproximationEx.thy Thu Feb 26 20:57:59 2009 +0100
@@ -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