--- a/NEWS Wed Mar 10 13:44:55 1999 +0100
+++ b/NEWS Wed Mar 10 16:31:33 1999 +0100
@@ -22,41 +22,51 @@
*** Proof tools ***
-* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
-procedure for linear arithmetic. Currently it is used for types `nat' and
-`int' in HOL (see below) but can, should and will be instantiated for other
-types and logics as well.
+* Provers/Arith/fast_lin_arith.ML contains a functor for creating a
+decision procedure for linear arithmetic. Currently it is used for
+types `nat' and `int' in HOL (see below) but can, should and will be
+instantiated for other types and logics as well.
*** General ***
-* in locales, the "assumes" and "defines" parts may be omitted if empty;
+* in locales, the "assumes" and "defines" parts may be omitted if
+empty;
* new print_mode "xsymbols" for extended symbol support (e.g. genuine
long arrows);
+* new print_mode "HTML";
+
* path element specification '~~' refers to '$ISABELLE_HOME';
+* new flag show_tags controls display of tags of theorems (which are
+basically just comments that may be attached by some tools);
+
*** HOL ***
-* There are now decision procedures for linear arithmetic over nat and int:
+* There are now decision procedures for linear arithmetic over nat and
+int:
-1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
-`-', `Suc', `min', `max' and numerical constants; other subterms are treated
-as atomic; subformulae not involving type `nat' or `int' are ignored;
-quantified subformulae are ignored unless they are positive universal or
-negative existential. The tactic has to be invoked by hand and can be a
-little bit slow. In particular, the running time is exponential in the number
-of occurrences of `min' and `max', and `-' on `nat'.
+1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
+`+', `-', `Suc', `min', `max' and numerical constants; other subterms
+are treated as atomic; subformulae not involving type `nat' or `int'
+are ignored; quantified subformulae are ignored unless they are
+positive universal or negative existential. The tactic has to be
+invoked by hand and can be a little bit slow. In particular, the
+running time is exponential in the number of occurrences of `min' and
+`max', and `-' on `nat'.
-2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
-(in)equalities among the premises and the conclusion into account (i.e. no
-compound formulae) and does not know about `min' and `max', and `-' on
-`nat'. It is fast and is used automatically by the simplifier.
+2. fast_arith_tac is a cut-down version of arith_tac: it only takes
+(negated) (in)equalities among the premises and the conclusion into
+account (i.e. no compound formulae) and does not know about `min' and
+`max', and `-' on `nat'. It is fast and is used automatically by the
+simplifier.
-NB: At the moment, these decision procedures do not cope with mixed nat/int
-formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
+NB: At the moment, these decision procedures do not cope with mixed
+nat/int formulae where the two parts interact, such as `m < n ==>
+int(m) < int(n)'.
* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
-- avoids syntactic ambiguities and treats state, transition, and
@@ -64,21 +74,6 @@
changed syntax and (many) tactics;
-*** Internal programming interfaces ***
-
-* tuned current_goals_markers semantics: begin / end goal avoids
-printing empty lines;
-
-* removed prs and prs_fn hook, which was broken because it did not
-include \n in its semantics, forcing writeln to add one
-uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
-string -> unit if you really want to output text without newline;
-
-* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
-plain output, interface builders may have to enable 'isabelle_font'
-mode to get Isabelle font glyphs as before;
-
-
*** ZF ***
* new primrec section allows primitive recursive functions to be given
@@ -102,6 +97,24 @@
if(P,x,y);
+*** Internal programming interfaces ***
+
+* tuned current_goals_markers semantics: begin / end goal avoids
+printing empty lines;
+
+* removed prs and prs_fn hook, which was broken because it did not
+include \n in its semantics, forcing writeln to add one
+uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
+string -> unit if you really want to output text without newline;
+
+* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
+plain output, interface builders may have to enable 'isabelle_font'
+mode to get Isabelle font glyphs as before;
+
+* refined token_translation interface; INCOMPATIBILITY: output length
+now of type real instead of int;
+
+
New in Isabelle98-1 (October 1998)
----------------------------------
--- a/doc-src/Ref/introduction.tex Wed Mar 10 13:44:55 1999 +0100
+++ b/doc-src/Ref/introduction.tex Wed Mar 10 16:31:33 1999 +0100
@@ -71,8 +71,8 @@
isabelle Foo
\end{ttbox}
-More details about the \texttt{isabelle} command may be found in the
-\emph{System Manual}.
+More details about the \texttt{isabelle} command may be found in \emph{The
+ Isabelle System Manual}.
\medskip Saving the state is not enough. Record, on a file, the
top-level commands that generate your theories and proofs. Such a
@@ -135,11 +135,12 @@
performs {\tt use~"$file$"} and prints the total execution time.
\end{ttdescription}
-The $dir$ and $file$ specifications of the \texttt{cd} and
-\texttt{use} commands may contain path variables that are expanded
-appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
-(which abbreviates \texttt{\$HOME}). Section~\ref{LoadingTheories}
-describes commands for loading theory files.
+The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
+commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
+expanded appropriately. Note that \texttt{\~\relax} abbreviates
+\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
+\texttt{\$ISABELLE_HOME}. Section~\ref{LoadingTheories} describes commands
+for loading theory files.
\section{Setting flags}
@@ -189,6 +190,7 @@
\index{types!printing of}\index{sorts!printing of}
\begin{ttbox}
show_hyps : bool ref \hfill{\bf initially true}
+show_tags : bool ref \hfill{\bf initially false}
show_brackets : bool ref \hfill{\bf initially false}
show_types : bool ref \hfill{\bf initially false}
show_sorts : bool ref \hfill{\bf initially false}
@@ -209,6 +211,9 @@
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
meta-level hypothesis as a dot.
+\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
+ (which are basically just comments that may be attached by some tools).
+
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
bracketing. In particular, this reveals the grouping of infix
operators.
--- a/doc-src/Ref/ref.ind Wed Mar 10 13:44:55 1999 +0100
+++ b/doc-src/Ref/ref.ind Wed Mar 10 16:31:33 1999 +0100
@@ -280,7 +280,7 @@
\subitem of simplification, 117
\subitem of translations, 98
\item exceptions
- \subitem printing of, 5
+ \subitem printing of, 6
\item {\tt exit}, \bold{2}
\item {\tt extensional}, \bold{48}
@@ -409,7 +409,7 @@
\item {\tt logic} nonterminal, \bold{72}
\item {\tt Logic.auto_rename}, \bold{25}
\item {\tt Logic.set_rename_prefix}, \bold{24}
- \item {\tt long_names}, \bold{4}
+ \item {\tt long_names}, \bold{5}
\item {\tt loose_bnos}, \bold{63}, 99
\indexspace
@@ -476,7 +476,7 @@
\item {\tt parse_rules}, 92
\item pattern, higher-order, \bold{110}
\item {\tt pause_tac}, \bold{29}
- \item Poly/{\ML} compiler, 5
+ \item Poly/{\ML} compiler, 6
\item {\tt pop_proof}, \bold{16}
\item {\tt pr}, \bold{12}
\item {\tt premises}, \bold{8}, 16
@@ -637,9 +637,10 @@
\subitem for \texttt{by} commands, 13
\subitem for tactics, 22
\item {\tt show_brackets}, \bold{4}
- \item {\tt show_consts}, \bold{4}
+ \item {\tt show_consts}, \bold{5}
\item {\tt show_hyps}, \bold{4}
\item {\tt show_sorts}, \bold{4}, 89, 97
+ \item {\tt show_tags}, \bold{4}
\item {\tt show_types}, \bold{4}, 89, 92, 99
\item {\tt Sign.certify_term}, \bold{65}
\item {\tt Sign.certify_typ}, \bold{66}
--- a/doc-src/Ref/syntax.tex Wed Mar 10 13:44:55 1999 +0100
+++ b/doc-src/Ref/syntax.tex Wed Mar 10 16:31:33 1999 +0100
@@ -712,13 +712,12 @@
which triggers calls to it. Such names can be constants (logical or
syntactic) or type constructors.
-{\tt print_syntax} displays the sets of names associated with the translation
-functions of a theory under \texttt{parse_ast_translation}, etc. You can add
-new ones via the {\tt ML} section\index{*ML section} of a theory definition
-file. There may never be more than one function of the same kind per name.
-Even though the {\tt ML} section is the very last part of the file, newly
-installed translation functions are already effective when processing all of
-the preceding sections.
+Function {\tt print_syntax} displays the sets of names associated with the
+translation functions of a theory under \texttt{parse_ast_translation}, etc.
+You can add new ones via the {\tt ML} section\index{*ML section} of a theory
+definition file. Even though the {\tt ML} section is the very last part of
+the file, newly installed translation functions are already effective when
+processing all of the preceding sections.
The {\tt ML} section's contents are simply copied verbatim near the
beginning of the \ML\ file generated from a theory definition file.
@@ -757,16 +756,18 @@
functions called during the parsing process differ from those for
printing more fundamentally in their overall behaviour:
\begin{description}
-\item[Parse translations] are applied bottom-up. The arguments are already
- in translated form. The translations must not fail; exceptions trigger
- an error message.
-
+\item[Parse translations] are applied bottom-up. The arguments are already in
+ translated form. The translations must not fail; exceptions trigger an
+ error message. There may never be more than one function associated with
+ any syntactic name.
+
\item[Print translations] are applied top-down. They are supplied with
arguments that are partly still in internal form. The result again
- undergoes translation; therefore a print translation should not introduce
- as head the very constant that invoked it. The function may raise
- exception \xdx{Match} to indicate failure; in this event it has no
- effect.
+ undergoes translation; therefore a print translation should not introduce as
+ head the very constant that invoked it. The function may raise exception
+ \xdx{Match} to indicate failure; in this event it has no effect. Multiple
+ functions associated with some syntactic name are tried in an unspecified
+ order.
\end{description}
Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
@@ -883,22 +884,21 @@
example at the end of \S\ref{sec:tr_funs}).
\medskip Token translations may be installed by declaring the
-\ttindex{token_translation} value within the \texttt{ML} section of a
-theory definition file:
+\ttindex{token_translation} value within the \texttt{ML} section of a theory
+definition file:
\begin{ttbox}
-val token_translation: (string * string * (string -> string * int)) list
+val token_translation: (string * string * (string -> string * real)) list
\end{ttbox}\index{token_translation}
-The elements of this list are of the form $(m, c, f)$, where $m$ is a
-print mode identifier, $c$ a token class, and $f\colon string \to
-string \times int$ the actual translation function. Assuming that $x$
-is of identifier class $c$, and print mode $m$ is the first one of all
-currently active modes that provide some translation for $c$, then $x$
-is output according to $f(x) = (x', len)$. Thereby $x'$ is the
-modified identifier name and $len$ its visual length approximated in
-terms of whole characters. Thus $x'$ may include non-printing parts
-like control sequences or markup information for typesetting systems.
+The elements of this list are of the form $(m, c, f)$, where $m$ is a print
+mode identifier, $c$ a token class, and $f\colon string \to string \times
+real$ the actual translation function. Assuming that $x$ is of identifier
+class $c$, and print mode $m$ is the first (active) mode providing some
+translation for $c$, then $x$ is output according to $f(x) = (x', len)$.
+Thereby $x'$ is the modified identifier name and $len$ its visual length in
+terms of characters (e.g.\ length 1.0 would correspond to $1/2$\,em in
+\LaTeX). Thus $x'$ may include non-printing parts like control sequences or
+markup information for typesetting systems.
-%FIXME example (?)
\index{token translations|)}