--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Sep 12 17:45:58 2006 +0200
@@ -13,7 +13,7 @@
chapter {* Basic library functions *}
-text {* FIXME beyond the basis library definition *}
+text {* FIXME beyond the NJ basis library proposal *}
chapter {* Cookbook *}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 12 17:45:58 2006 +0200
@@ -35,7 +35,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME beyond the basis library definition%
+FIXME beyond the NJ basis library proposal%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/isar.tex Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/isar.tex Tue Sep 12 17:45:58 2006 +0200
@@ -23,7 +23,16 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Proof states \label{sec:isar-proof-state}%
+\isamarkupsection{Proof context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof state \label{sec:isar-proof-state}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/locale.tex Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/locale.tex Tue Sep 12 17:45:58 2006 +0200
@@ -32,7 +32,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Type-checking specifications%
+\isamarkupsection{Type-inference%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:45:58 2006 +0200
@@ -132,9 +132,9 @@
\indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
\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: (bstring * int * mixfix) list -> theory -> theory| \\
+ \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%
-\verb| (bstring * string list * typ * mixfix) list -> theory -> theory| \\
+\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| \\
@@ -201,11 +201,11 @@
\glossary{Term}{FIXME}
The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
- with de-Bruijn indices for bound variables
- \cite{debruijn72,paulson-ml2}, and named free variables and
- constants. Terms with loose bound variables are usually considered
- malformed. The types of variables and constants is stored
- explicitly at each occurrence in the term.
+ with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
+ or \cite{paulson-ml2}), and named free variables and constants.
+ Terms with loose bound variables are usually considered malformed.
+ The types of variables and constants is stored explicitly at each
+ occurrence in the term.
\medskip A \emph{bound variable} is a natural number \isa{b},
which refers to the next binder that is \isa{b} steps upwards
@@ -319,9 +319,9 @@
\indexml{fastype-of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (bstring * typ * mixfix) list -> theory -> theory| \\
+ \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
\indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
-\verb| ((bstring * mixfix) * term) list -> theory -> theory| \\
+\verb| ((string * mixfix) * term) list -> theory -> 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| \\
\end{mldecls}
@@ -356,10 +356,10 @@
well-formed term, while omitting any sanity checks. This operation
is relatively slow.
- \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the original (atomic) term \isa{a} are replaced by bound variables.
+ \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the original (atomic) term \isa{a} in the body \isa{b} are replaced by bound variables.
- \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion \isa{t} is an
- abstraction.
+ \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} happens to
+ be an abstraction.
\item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
@@ -368,11 +368,10 @@
declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional
mixfix syntax.
- \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} produces the
- type arguments of the instance \isa{c\isactrlisub {\isasymtau}} wrt.\ its
- declaration in the theory.
-
- \item \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}} produces the full instance \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} wrt.\ its declaration in the theory.
+ \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
+ convert between the two representations of constants, namely full
+ type instance vs.\ compact type arguments form (depending on the
+ most general declaration given in the context).
\end{description}%
\end{isamarkuptext}%
@@ -481,7 +480,7 @@
option to control the generation of full proof terms.
\medskip The axiomatization of a theory is implicitly closed by
- forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymtheta}} for
+ forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} for
any substitution instance of axiom \isa{{\isasymturnstile}\ A}. By pushing
substitution through derivations inductively, we get admissible
substitution rules for theorems shown in \figref{fig:subst-rules}.
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Tue Sep 12 17:45:58 2006 +0200
@@ -278,7 +278,7 @@
%
\endisadelimmlref
%
-\isamarkupsection{Conclusions%
+\isamarkupsection{Results%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/isar.thy Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/isar.thy Tue Sep 12 17:45:58 2006 +0200
@@ -5,7 +5,12 @@
chapter {* Isar proof texts *}
-section {* Proof states \label{sec:isar-proof-state} *}
+section {* Proof context *}
+
+text FIXME
+
+
+section {* Proof state \label{sec:isar-proof-state} *}
text {*
FIXME
--- a/doc-src/IsarImplementation/Thy/locale.thy Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/locale.thy Tue Sep 12 17:45:58 2006 +0200
@@ -10,7 +10,7 @@
text FIXME
-section {* Type-checking specifications *}
+section {* Type-inference *}
text FIXME
--- a/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:45:58 2006 +0200
@@ -126,9 +126,9 @@
@{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
- @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
@{index_ML Sign.add_tyabbrs_i: "
- (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
+ (string * string list * typ * mixfix) list -> theory -> theory"} \\
@{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
@{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
@{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
@@ -192,11 +192,11 @@
\glossary{Term}{FIXME}
The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
- with de-Bruijn indices for bound variables
- \cite{debruijn72,paulson-ml2}, and named free variables and
- constants. Terms with loose bound variables are usually considered
- malformed. The types of variables and constants is stored
- explicitly at each occurrence in the term.
+ with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
+ or \cite{paulson-ml2}), and named free variables and constants.
+ Terms with loose bound variables are usually considered malformed.
+ The types of variables and constants is stored explicitly at each
+ occurrence in the term.
\medskip A \emph{bound variable} is a natural number @{text "b"},
which refers to the next binder that is @{text "b"} steps upwards
@@ -317,9 +317,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
@{index_ML Sign.add_abbrevs: "string * bool ->
- ((bstring * mixfix) * term) list -> theory -> theory"} \\
+ ((string * mixfix) * term) list -> theory -> theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
\end{mldecls}
@@ -358,11 +358,11 @@
\item @{ML lambda}~@{text "a b"} produces an abstraction @{text
"\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
- "a"} are replaced by bound variables.
+ "a"} in the body @{text "b"} are replaced by bound variables.
\item @{ML betapply}~@{text "t u"} produces an application @{text "t
- u"}, with topmost @{text "\<beta>"}-conversion @{text "t"} is an
- abstraction.
+ u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to
+ be an abstraction.
\item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
@@ -371,13 +371,11 @@
declares a new term abbreviation @{text "c \<equiv> t"} with optional
mixfix syntax.
- \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} produces the
- type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its
- declaration in the theory.
-
- \item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,
- \<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,
- \<tau>\<^isub>n)"} wrt.\ its declaration in the theory.
+ \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
+ Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
+ convert between the two representations of constants, namely full
+ type instance vs.\ compact type arguments form (depending on the
+ most general declaration given in the context).
\end{description}
*}
@@ -479,7 +477,7 @@
option to control the generation of full proof terms.
\medskip The axiomatization of a theory is implicitly closed by
- forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
+ forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
any substitution instance of axiom @{text "\<turnstile> A"}. By pushing
substitution through derivations inductively, we get admissible
substitution rules for theorems shown in \figref{fig:subst-rules}.
--- a/doc-src/IsarImplementation/Thy/proof.thy Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Tue Sep 12 17:45:58 2006 +0200
@@ -247,7 +247,7 @@
*}
-section {* Conclusions *}
+section {* Results *}
text {*
Local results are established by monotonic reasoning from facts