--- a/Admin/isatest/settings/sun-poly Thu Feb 26 18:00:08 2009 +0100
+++ b/Admin/isatest/settings/sun-poly Fri Feb 27 08:12:38 2009 +0100
@@ -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
--- a/Admin/makedist Thu Feb 26 18:00:08 2009 +0100
+++ b/Admin/makedist Fri Feb 27 08:12:38 2009 +0100
@@ -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}
--- a/doc-src/Intro/intro.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/Intro/intro.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/style.sty Fri Feb 27 08:12:38 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/IsaMakefile Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/IsaMakefile Fri Feb 27 08:12:38 2009 +0100
@@ -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
--- a/doc-src/IsarImplementation/Makefile Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Makefile Fri Feb 27 08:12:38 2009 +0100
@@ -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
--- a/doc-src/IsarImplementation/Thy/ROOT.ML Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML Fri Feb 27 08:12:38 2009 +0100
@@ -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"
+];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy Fri Feb 27 08:12:38 2009 +0100
@@ -0,0 +1,9 @@
+theory Syntax
+imports Base
+begin
+
+chapter {* Syntax and type-checking *}
+
+text FIXME
+
+end
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Fri Feb 27 08:12:38 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}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Fri Feb 27 08:12:38 2009 +0100
@@ -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:
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Fri Feb 27 08:12:38 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/Thy/document/session.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/session.tex Fri Feb 27 08:12:38 2009 +0100
@@ -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"
--- a/doc-src/IsarImplementation/implementation.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex Fri Feb 27 08:12:38 2009 +0100
@@ -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
--- a/doc-src/IsarImplementation/style.sty Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarImplementation/style.sty Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Feb 27 08:12:38 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/isar-ref.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Fri Feb 27 08:12:38 2009 +0100
@@ -104,7 +104,7 @@
\input{Thy/document/ML_Tactic.tex}
\begingroup
- \bibliographystyle{plain} \small\raggedright\frenchspacing
+ \bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
--- a/doc-src/IsarRef/style.sty Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/IsarRef/style.sty Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/doc-src/Ref/ref.tex Fri Feb 27 08:12:38 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/System/system.tex Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/System/system.tex Fri Feb 27 08:12:38 2009 +0100
@@ -36,7 +36,7 @@
\input{Thy/document/Misc.tex}
\begingroup
- \bibliographystyle{plain} \small\raggedright\frenchspacing
+ \bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
--- a/doc-src/antiquote_setup.ML Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/antiquote_setup.ML Fri Feb 27 08:12:38 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-src/manual.bib Thu Feb 26 18:00:08 2009 +0100
+++ b/doc-src/manual.bib Fri Feb 27 08:12:38 2009 +0100
@@ -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}},
--- a/doc/Contents Thu Feb 26 18:00:08 2009 +0100
+++ b/doc/Contents Fri Feb 27 08:12:38 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 18:00:08 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Feb 27 08:12:38 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/Bit.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/Library/Bit.thy Fri Feb 27 08:12:38 2009 +0100
@@ -79,14 +79,8 @@
end
-lemma bit_1_plus_1 [simp]: "1 + 1 = (0 :: bit)"
- unfolding plus_bit_def by simp
-
-lemma bit_add_self [simp]: "x + x = (0 :: bit)"
- by (cases x) simp_all
-
-lemma bit_add_self_left [simp]: "x + (x + y) = (y :: bit)"
- by simp
+lemma bit_add_self: "x + x = (0 :: bit)"
+ unfolding plus_bit_def by (simp split: bit.split)
lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
unfolding times_bit_def by (simp split: bit.split)
--- a/src/HOL/Library/Float.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/Library/Float.thy Fri Feb 27 08:12:38 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/List.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/List.thy Fri Feb 27 08:12:38 2009 +0100
@@ -1438,10 +1438,10 @@
apply (auto split:nat.split)
done
-lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
by(induct xs)(auto simp:neq_Nil_conv)
-lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
+lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
by (induct xs, simp, case_tac xs, simp_all)
@@ -1461,6 +1461,12 @@
declare take_Cons [simp del] and drop_Cons [simp del]
+lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
+ unfolding One_nat_def by simp
+
+lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
+ unfolding One_nat_def by simp
+
lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
by(clarsimp simp add:neq_Nil_conv)
@@ -1588,17 +1594,17 @@
done
lemma butlast_take:
- "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
+ "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take)
+by (simp add: butlast_conv_take drop_take add_ac)
lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
by (simp add: butlast_conv_take min_max.inf_absorb1)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take)
+by (simp add: butlast_conv_take drop_take add_ac)
lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
by(simp add: hd_conv_nth)
@@ -2458,7 +2464,7 @@
done
lemma length_remove1:
- "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
+ "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
apply (induct xs)
apply (auto dest!:length_pos_if_in_set)
done
--- a/src/HOL/Nat.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/Nat.thy Fri Feb 27 08:12:38 2009 +0100
@@ -701,6 +701,9 @@
lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
by (simp add: diff_Suc split: nat.split)
+lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
+unfolding One_nat_def by (rule Suc_pred)
+
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
by (induct k) simp_all
@@ -1135,7 +1138,7 @@
by (cases m) (auto intro: le_add1)
text {* Lemma for @{text gcd} *}
-lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
+lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
apply (drule sym)
apply (rule disjCI)
apply (rule nat_less_cases, erule_tac [2] _)
--- a/src/HOL/RComplete.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/RComplete.thy Fri Feb 27 08:12:38 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/ROOT.ML Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/ROOT.ML Fri Feb 27 08:12:38 2009 +0100
@@ -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;
--- a/src/HOL/ex/ApproximationEx.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOL/ex/ApproximationEx.thy Fri Feb 27 08:12:38 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
--- a/src/HOLCF/Fixrec.thy Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOLCF/Fixrec.thy Fri Feb 27 08:12:38 2009 +0100
@@ -583,6 +583,20 @@
use "Tools/fixrec_package.ML"
+setup {* FixrecPackage.setup *}
+
+setup {*
+ FixrecPackage.add_matchers
+ [ (@{const_name up}, @{const_name match_up}),
+ (@{const_name sinl}, @{const_name match_sinl}),
+ (@{const_name sinr}, @{const_name match_sinr}),
+ (@{const_name spair}, @{const_name match_spair}),
+ (@{const_name cpair}, @{const_name match_cpair}),
+ (@{const_name ONE}, @{const_name match_ONE}),
+ (@{const_name TT}, @{const_name match_TT}),
+ (@{const_name FF}, @{const_name match_FF}) ]
+*}
+
hide (open) const return bind fail run cases
end
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Fri Feb 27 08:12:38 2009 +0100
@@ -39,7 +39,7 @@
fun one_con (con,args) =
foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
in ("copy_def", %%:(dname^"_copy") ==
- /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
+ /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
(* -- definitions concerning the constructors, discriminators and selectors - *)
@@ -107,7 +107,7 @@
[when_def, copy_def] @
con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
[take_def, finite_def])
-end; (* let *)
+end; (* let (calc_axioms) *)
fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
@@ -117,6 +117,14 @@
fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
+fun add_matchers (((dname,_),cons) : eq) thy =
+ let
+ val con_names = map fst cons;
+ val mat_names = map mat_name con_names;
+ fun qualify n = Sign.full_name thy (Binding.name n);
+ val ms = map qualify con_names ~~ map qualify mat_names;
+ in FixrecPackage.add_matchers ms thy end;
+
in (* local *)
fun add_axioms (comp_dnam, eqs : eq list) thy' = let
@@ -125,7 +133,7 @@
val x_name = idx_name dnames "x";
fun copy_app dname = %%:(dname^"_copy")`Bound 0;
val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
- /\"f"(mk_ctuple (map copy_app dnames)));
+ /\ "f"(mk_ctuple (map copy_app dnames)));
val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
let
fun one_con (con,args) = let
@@ -164,7 +172,8 @@
in thy |> Sign.add_path comp_dnam
|> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
|> Sign.parent_path
-end;
+ |> fold add_matchers eqs
+end; (* let (add_axioms) *)
end; (* local *)
end; (* struct *)
--- a/src/HOLCF/Tools/fixrec_package.ML Thu Feb 26 18:00:08 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Fri Feb 27 08:12:38 2009 +0100
@@ -8,17 +8,20 @@
sig
val legacy_infer_term: theory -> term -> term
val legacy_infer_prop: theory -> term -> term
+
val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
val add_fixpat: Attrib.binding * string list -> theory -> theory
val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
+ val add_matchers: (string * string) list -> theory -> theory
+ val setup: theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
struct
(* legacy type inference *)
-
+(* used by the domain package *)
fun legacy_infer_term thy t =
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
@@ -33,15 +36,41 @@
fun fixrec_eq_err thy s eq =
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
+(*************************************************************************)
+(***************************** building types ****************************)
+(*************************************************************************)
+
(* ->> is taken from holcf_logic.ML *)
-(* TODO: fix dependencies so we can import HOLCFLogic here *)
-infixr 6 ->>;
-fun S ->> T = Type (@{type_name "->"},[S,T]);
+fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+infixr 6 ->>; val (op ->>) = cfunT;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+ | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+ | binder_cfun _ = [];
+
+fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+ | body_cfun T = T;
-(* extern_name is taken from domain/library.ML *)
-fun extern_name con = case Symbol.explode con of
- ("o"::"p"::" "::rest) => implode rest
- | _ => con;
+fun strip_cfun T : typ list * typ =
+ (binder_cfun T, body_cfun T);
+
+fun maybeT T = Type(@{type_name "maybe"}, [T]);
+
+fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
+ | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
+
+fun tupleT [] = @{typ "unit"}
+ | tupleT [T] = T
+ | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
+
+fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T));
+
+(*************************************************************************)
+(***************************** building terms ****************************)
+(*************************************************************************)
val mk_trp = HOLogic.mk_Trueprop;
@@ -52,30 +81,86 @@
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
| chead_of u = u;
-(* these are helpful functions copied from HOLCF/domain/library.ML *)
-fun %: s = Free(s,dummyT);
-fun %%: s = Const(s,dummyT);
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 9 ` ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
+fun capply_const (S, T) =
+ Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+
+fun cabs_const (S, T) =
+ Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+
+fun mk_capply (t, u) =
+ let val (S, T) =
+ case Term.fastype_of t of
+ Type(@{type_name "->"}, [S, T]) => (S, T)
+ | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
+ in capply_const (S, T) $ t $ u end;
+
+infix 0 ==; val (op ==) = Logic.mk_equals;
+infix 1 ===; val (op ===) = HOLogic.mk_eq;
+infix 9 ` ; val (op `) = mk_capply;
+
+
+fun mk_cpair (t, u) =
+ let val T = Term.fastype_of t
+ val U = Term.fastype_of u
+ val cpairT = T ->> U ->> HOLogic.mk_prodT (T, U)
+ in Const(@{const_name cpair}, cpairT) ` t ` u end;
+
+fun mk_cfst t =
+ let val T = Term.fastype_of t;
+ val (U, _) = HOLogic.dest_prodT T;
+ in Const(@{const_name cfst}, T ->> U) ` t end;
+
+fun mk_csnd t =
+ let val T = Term.fastype_of t;
+ val (_, U) = HOLogic.dest_prodT T;
+ in Const(@{const_name csnd}, T ->> U) ` t end;
+
+fun mk_csplit t =
+ let val (S, TU) = dest_cfunT (Term.fastype_of t);
+ val (T, U) = dest_cfunT TU;
+ val csplitT = (S ->> T ->> U) ->> HOLogic.mk_prodT (S, T) ->> U;
+ in Const(@{const_name csplit}, csplitT) ` t end;
(* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs = %%:@{const_name Abs_CFun}$(Term.lambda v rhs);
+fun big_lambda v rhs =
+ cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
(* builds the expression (LAM v1 v2 .. vn. rhs) *)
fun big_lambdas [] rhs = rhs
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
(* builds the expression (LAM <v1,v2,..,vn>. rhs) *)
-fun lambda_ctuple [] rhs = big_lambda (%:"unit") rhs
+fun lambda_ctuple [] rhs = big_lambda (Free("unit", HOLogic.unitT)) rhs
| lambda_ctuple (v::[]) rhs = big_lambda v rhs
| lambda_ctuple (v::vs) rhs =
- %%:@{const_name csplit}`(big_lambda v (lambda_ctuple vs rhs));
+ mk_csplit (big_lambda v (lambda_ctuple vs rhs));
(* builds the expression <v1,v2,..,vn> *)
-fun mk_ctuple [] = %%:"UU"
+fun mk_ctuple [] = @{term "UU::unit"}
| mk_ctuple (t::[]) = t
-| mk_ctuple (t::ts) = %%:@{const_name cpair}`t`(mk_ctuple ts);
+| mk_ctuple (t::ts) = mk_cpair (t, mk_ctuple ts);
+
+fun mk_return t =
+ let val T = Term.fastype_of t
+ in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
+
+fun mk_bind (t, u) =
+ let val (T, mU) = dest_cfunT (Term.fastype_of u);
+ val bindT = maybeT T ->> (T ->> mU) ->> mU;
+ in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
+
+fun mk_mplus (t, u) =
+ let val mT = Term.fastype_of t
+ in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
+
+fun mk_run t =
+ let val mT = Term.fastype_of t
+ val T = dest_maybeT mT
+ in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
+
+fun mk_fix t =
+ let val (T, _) = dest_cfunT (Term.fastype_of t)
+ in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
(*************************************************************************)
(************* fixed-point definitions and unfolding theorems ************)
@@ -84,22 +169,21 @@
fun add_fixdefs eqs thy =
let
val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs);
- val fixpoint = %%:@{const_name fix}`lambda_ctuple lhss (mk_ctuple rhss);
+ val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
fun one_def (l as Const(n,T)) r =
let val b = Sign.base_name n in (b, (b^"_def", l == r)) end
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
fun defs [] _ = []
| defs (l::[]) r = [one_def l r]
- | defs (l::ls) r = one_def l (%%:@{const_name cfst}`r) :: defs ls (%%:@{const_name csnd}`r);
- val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
+ | defs (l::ls) r = one_def l (mk_cfst r) :: defs ls (mk_csnd r);
+ val (names, fixdefs) = ListPair.unzip (defs lhss fixpoint);
- val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
val (fixdef_thms, thy') =
PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) fixdefs) thy;
val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
- val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
+ val ctuple_unfold = mk_trp (mk_ctuple lhss === mk_ctuple rhss);
val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
(fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
simp_tac (simpset_of thy') 1]);
@@ -123,6 +207,17 @@
(*********** monadic notation and pattern matching compilation ***********)
(*************************************************************************)
+structure FixrecMatchData = TheoryDataFun (
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ tabs : T = Symtab.merge (K true) tabs;
+);
+
+(* associate match functions with pattern constants *)
+fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
+
fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
| add_names (Free(a,_) , bs) = insert (op =) a bs
| add_names (f $ u , bs) = add_names (f, add_names(u, bs))
@@ -132,56 +227,63 @@
fun add_terms ts xs = foldr add_names xs ts;
(* builds a monadic term for matching a constructor pattern *)
-fun pre_build pat rhs vs taken =
+fun pre_build match_name pat rhs vs taken =
case pat of
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
- pre_build f rhs (v::vs) taken
+ pre_build match_name f rhs (v::vs) taken
| Const(@{const_name Rep_CFun},_)$f$x =>
- let val (rhs', v, taken') = pre_build x rhs [] taken;
- in pre_build f rhs' (v::vs) taken' end
+ let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
+ in pre_build match_name f rhs' (v::vs) taken' end
| Const(c,T) =>
let
val n = Name.variant taken "v";
fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
| result_type T _ = T;
val v = Free(n, result_type T vs);
- val m = "match_"^(extern_name(Sign.base_name c));
+ val m = Const(match_name c, matchT T);
val k = lambda_ctuple vs rhs;
in
- (%%:@{const_name Fixrec.bind}`(%%:m`v)`k, v, n::taken)
+ (mk_bind (m`v, k), v, n::taken)
end
| Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
| _ => fixrec_err "pre_build: invalid pattern";
(* builds a monadic term for matching a function definition pattern *)
(* returns (name, arity, matcher) *)
-fun building pat rhs vs taken =
+fun building match_name pat rhs vs taken =
case pat of
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
- building f rhs (v::vs) taken
+ building match_name f rhs (v::vs) taken
| Const(@{const_name Rep_CFun}, _)$f$x =>
- let val (rhs', v, taken') = pre_build x rhs [] taken;
- in building f rhs' (v::vs) taken' end
- | Const(name,_) => (name, length vs, big_lambdas vs rhs)
+ let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
+ in building match_name f rhs' (v::vs) taken' end
+ | Const(name,_) => (pat, length vs, big_lambdas vs rhs)
| _ => fixrec_err "function is not declared as constant in theory";
-fun match_eq eq =
+fun match_eq match_name eq =
let val (lhs,rhs) = dest_eqs eq;
- in building lhs (%%:@{const_name Fixrec.return}`rhs) [] (add_terms [eq] []) end;
+ in
+ building match_name lhs (mk_return rhs) []
+ (add_terms [eq] [])
+ end;
(* returns the sum (using +++) of the terms in ms *)
(* also applies "run" to the result! *)
fun fatbar arity ms =
let
+ fun LAM_Ts 0 t = ([], Term.fastype_of t)
+ | LAM_Ts n (_ $ Abs(_,T,t)) =
+ let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
+ | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
fun unLAM 0 t = t
| unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
| unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
- fun reLAM 0 t = t
- | reLAM n t = reLAM (n-1) (%%:@{const_name Abs_CFun} $ Abs("",dummyT,t));
- fun mplus (x,y) = %%:@{const_name Fixrec.mplus}`x`y;
- val msum = foldr1 mplus (map (unLAM arity) ms);
+ fun reLAM ([], U) t = t
+ | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
+ val msum = foldr1 mk_mplus (map (unLAM arity) ms);
+ val (Ts, U) = LAM_Ts arity (hd ms)
in
- reLAM arity (%%:@{const_name Fixrec.run}`msum)
+ reLAM (rev Ts, dest_maybeT U) (mk_run msum)
end;
fun unzip3 [] = ([],[],[])
@@ -190,16 +292,16 @@
in (x::xs, y::ys, z::zs) end;
(* this is the pattern-matching compiler function *)
-fun compile_pats eqs =
+fun compile_pats match_name eqs =
let
- val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs);
+ val ((n::names),(a::arities),mats) = unzip3 (map (match_eq match_name) eqs);
val cname = if forall (fn x => n=x) names then n
else fixrec_err "all equations in block must define the same function";
val arity = if forall (fn x => a=x) arities then a
else fixrec_err "all equations in block must have the same arity";
val rhs = fatbar arity mats;
in
- mk_trp (%%:cname === rhs)
+ mk_trp (cname === rhs)
end;
(*************************************************************************)
@@ -235,8 +337,14 @@
fun unconcat [] _ = []
| unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));
+ val matcher_tab = FixrecMatchData.get thy;
+ fun match_name c =
+ case Symtab.lookup matcher_tab c of SOME m => m
+ | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
+
val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts');
- val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks;
+ val compiled_ts =
+ map (compile_pats match_name) pattern_blocks;
val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy;
in
if strict then let (* only prove simp rules if strict = true *)
@@ -312,4 +420,6 @@
end; (* local structure *)
+val setup = FixrecMatchData.init;
+
end;