updated;
authorwenzelm
Wed Mar 10 16:31:33 1999 +0100 (1999-03-10)
changeset 634397c697a32b73
parent 6342 13424bbc2d8b
child 6344 9442bc6763f7
updated;
NEWS
doc-src/Ref/introduction.tex
doc-src/Ref/ref.ind
doc-src/Ref/syntax.tex
     1.1 --- a/NEWS	Wed Mar 10 13:44:55 1999 +0100
     1.2 +++ b/NEWS	Wed Mar 10 16:31:33 1999 +0100
     1.3 @@ -22,41 +22,51 @@
     1.4  
     1.5  *** Proof tools ***
     1.6  
     1.7 -* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
     1.8 -procedure for linear arithmetic. Currently it is used for types `nat' and
     1.9 -`int' in HOL (see below) but can, should and will be instantiated for other
    1.10 -types and logics as well.
    1.11 +* Provers/Arith/fast_lin_arith.ML contains a functor for creating a
    1.12 +decision procedure for linear arithmetic. Currently it is used for
    1.13 +types `nat' and `int' in HOL (see below) but can, should and will be
    1.14 +instantiated for other types and logics as well.
    1.15  
    1.16  
    1.17  *** General ***
    1.18  
    1.19 -* in locales, the "assumes" and "defines" parts may be omitted if empty;
    1.20 +* in locales, the "assumes" and "defines" parts may be omitted if
    1.21 +empty;
    1.22  
    1.23  * new print_mode "xsymbols" for extended symbol support (e.g. genuine
    1.24  long arrows);
    1.25  
    1.26 +* new print_mode "HTML";
    1.27 +
    1.28  * path element specification '~~' refers to '$ISABELLE_HOME';
    1.29  
    1.30 +* new flag show_tags controls display of tags of theorems (which are
    1.31 +basically just comments that may be attached by some tools);
    1.32 +
    1.33  
    1.34  *** HOL ***
    1.35  
    1.36 -* There are now decision procedures for linear arithmetic over nat and int:
    1.37 +* There are now decision procedures for linear arithmetic over nat and
    1.38 +int:
    1.39  
    1.40 -1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
    1.41 -`-', `Suc', `min', `max' and numerical constants; other subterms are treated
    1.42 -as atomic; subformulae not involving type `nat' or `int' are ignored;
    1.43 -quantified subformulae are ignored unless they are positive universal or
    1.44 -negative existential. The tactic has to be invoked by hand and can be a
    1.45 -little bit slow. In particular, the running time is exponential in the number
    1.46 -of occurrences of `min' and `max', and `-' on `nat'.
    1.47 +1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
    1.48 +`+', `-', `Suc', `min', `max' and numerical constants; other subterms
    1.49 +are treated as atomic; subformulae not involving type `nat' or `int'
    1.50 +are ignored; quantified subformulae are ignored unless they are
    1.51 +positive universal or negative existential. The tactic has to be
    1.52 +invoked by hand and can be a little bit slow. In particular, the
    1.53 +running time is exponential in the number of occurrences of `min' and
    1.54 +`max', and `-' on `nat'.
    1.55  
    1.56 -2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
    1.57 -(in)equalities among the premises and the conclusion into account (i.e. no
    1.58 -compound formulae) and does not know about `min' and `max', and `-' on
    1.59 -`nat'. It is fast and is used automatically by the simplifier.
    1.60 +2. fast_arith_tac is a cut-down version of arith_tac: it only takes
    1.61 +(negated) (in)equalities among the premises and the conclusion into
    1.62 +account (i.e. no compound formulae) and does not know about `min' and
    1.63 +`max', and `-' on `nat'. It is fast and is used automatically by the
    1.64 +simplifier.
    1.65  
    1.66 -NB: At the moment, these decision procedures do not cope with mixed nat/int
    1.67 -formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
    1.68 +NB: At the moment, these decision procedures do not cope with mixed
    1.69 +nat/int formulae where the two parts interact, such as `m < n ==>
    1.70 +int(m) < int(n)'.
    1.71  
    1.72  * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
    1.73  -- avoids syntactic ambiguities and treats state, transition, and
    1.74 @@ -64,21 +74,6 @@
    1.75  changed syntax and (many) tactics;
    1.76  
    1.77  
    1.78 -*** Internal programming interfaces ***
    1.79 -
    1.80 -* tuned current_goals_markers semantics: begin / end goal avoids
    1.81 -printing empty lines;
    1.82 -
    1.83 -* removed prs and prs_fn hook, which was broken because it did not
    1.84 -include \n in its semantics, forcing writeln to add one
    1.85 -uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
    1.86 -string -> unit if you really want to output text without newline;
    1.87 -
    1.88 -* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
    1.89 -plain output, interface builders may have to enable 'isabelle_font'
    1.90 -mode to get Isabelle font glyphs as before;
    1.91 -
    1.92 -
    1.93  *** ZF ***
    1.94  
    1.95  * new primrec section allows primitive recursive functions to be given
    1.96 @@ -102,6 +97,24 @@
    1.97  if(P,x,y);
    1.98  
    1.99  
   1.100 +*** Internal programming interfaces ***
   1.101 +
   1.102 +* tuned current_goals_markers semantics: begin / end goal avoids
   1.103 +printing empty lines;
   1.104 +
   1.105 +* removed prs and prs_fn hook, which was broken because it did not
   1.106 +include \n in its semantics, forcing writeln to add one
   1.107 +uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
   1.108 +string -> unit if you really want to output text without newline;
   1.109 +
   1.110 +* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
   1.111 +plain output, interface builders may have to enable 'isabelle_font'
   1.112 +mode to get Isabelle font glyphs as before;
   1.113 +
   1.114 +* refined token_translation interface; INCOMPATIBILITY: output length
   1.115 +now of type real instead of int;
   1.116 +
   1.117 +
   1.118  
   1.119  New in Isabelle98-1 (October 1998)
   1.120  ----------------------------------
     2.1 --- a/doc-src/Ref/introduction.tex	Wed Mar 10 13:44:55 1999 +0100
     2.2 +++ b/doc-src/Ref/introduction.tex	Wed Mar 10 16:31:33 1999 +0100
     2.3 @@ -71,8 +71,8 @@
     2.4  isabelle Foo  
     2.5  \end{ttbox}
     2.6  
     2.7 -More details about the \texttt{isabelle} command may be found in the
     2.8 -\emph{System Manual}.
     2.9 +More details about the \texttt{isabelle} command may be found in \emph{The
    2.10 +  Isabelle System Manual}.
    2.11  
    2.12  \medskip Saving the state is not enough.  Record, on a file, the
    2.13  top-level commands that generate your theories and proofs.  Such a
    2.14 @@ -135,11 +135,12 @@
    2.15  performs {\tt use~"$file$"} and prints the total execution time.
    2.16  \end{ttdescription}
    2.17  
    2.18 -The $dir$ and $file$ specifications of the \texttt{cd} and
    2.19 -\texttt{use} commands may contain path variables that are expanded
    2.20 -appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
    2.21 -(which abbreviates \texttt{\$HOME}).  Section~\ref{LoadingTheories}
    2.22 -describes commands for loading theory files.
    2.23 +The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
    2.24 +commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
    2.25 +expanded appropriately.  Note that \texttt{\~\relax} abbreviates
    2.26 +\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
    2.27 +\texttt{\$ISABELLE_HOME}.  Section~\ref{LoadingTheories} describes commands
    2.28 +for loading theory files.
    2.29  
    2.30  
    2.31  \section{Setting flags}
    2.32 @@ -189,6 +190,7 @@
    2.33  \index{types!printing of}\index{sorts!printing of}
    2.34  \begin{ttbox} 
    2.35  show_hyps     : bool ref \hfill{\bf initially true}
    2.36 +show_tags     : bool ref \hfill{\bf initially false}
    2.37  show_brackets : bool ref \hfill{\bf initially false}
    2.38  show_types    : bool ref \hfill{\bf initially false}
    2.39  show_sorts    : bool ref \hfill{\bf initially false}
    2.40 @@ -209,6 +211,9 @@
    2.41  \item[reset \ttindexbold{show_hyps};] makes Isabelle show each
    2.42    meta-level hypothesis as a dot.
    2.43    
    2.44 +\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
    2.45 +  (which are basically just comments that may be attached by some tools).
    2.46 +  
    2.47  \item[set \ttindexbold{show_brackets};] makes Isabelle show full
    2.48    bracketing.  In particular, this reveals the grouping of infix
    2.49    operators.
     3.1 --- a/doc-src/Ref/ref.ind	Wed Mar 10 13:44:55 1999 +0100
     3.2 +++ b/doc-src/Ref/ref.ind	Wed Mar 10 16:31:33 1999 +0100
     3.3 @@ -280,7 +280,7 @@
     3.4      \subitem of simplification, 117
     3.5      \subitem of translations, 98
     3.6    \item exceptions
     3.7 -    \subitem printing of, 5
     3.8 +    \subitem printing of, 6
     3.9    \item {\tt exit}, \bold{2}
    3.10    \item {\tt extensional}, \bold{48}
    3.11  
    3.12 @@ -409,7 +409,7 @@
    3.13    \item {\tt logic} nonterminal, \bold{72}
    3.14    \item {\tt Logic.auto_rename}, \bold{25}
    3.15    \item {\tt Logic.set_rename_prefix}, \bold{24}
    3.16 -  \item {\tt long_names}, \bold{4}
    3.17 +  \item {\tt long_names}, \bold{5}
    3.18    \item {\tt loose_bnos}, \bold{63}, 99
    3.19  
    3.20    \indexspace
    3.21 @@ -476,7 +476,7 @@
    3.22    \item {\tt parse_rules}, 92
    3.23    \item pattern, higher-order, \bold{110}
    3.24    \item {\tt pause_tac}, \bold{29}
    3.25 -  \item Poly/{\ML} compiler, 5
    3.26 +  \item Poly/{\ML} compiler, 6
    3.27    \item {\tt pop_proof}, \bold{16}
    3.28    \item {\tt pr}, \bold{12}
    3.29    \item {\tt premises}, \bold{8}, 16
    3.30 @@ -637,9 +637,10 @@
    3.31      \subitem for \texttt{by} commands, 13
    3.32      \subitem for tactics, 22
    3.33    \item {\tt show_brackets}, \bold{4}
    3.34 -  \item {\tt show_consts}, \bold{4}
    3.35 +  \item {\tt show_consts}, \bold{5}
    3.36    \item {\tt show_hyps}, \bold{4}
    3.37    \item {\tt show_sorts}, \bold{4}, 89, 97
    3.38 +  \item {\tt show_tags}, \bold{4}
    3.39    \item {\tt show_types}, \bold{4}, 89, 92, 99
    3.40    \item {\tt Sign.certify_term}, \bold{65}
    3.41    \item {\tt Sign.certify_typ}, \bold{66}
     4.1 --- a/doc-src/Ref/syntax.tex	Wed Mar 10 13:44:55 1999 +0100
     4.2 +++ b/doc-src/Ref/syntax.tex	Wed Mar 10 16:31:33 1999 +0100
     4.3 @@ -712,13 +712,12 @@
     4.4  which triggers calls to it.  Such names can be constants (logical or
     4.5  syntactic) or type constructors.
     4.6  
     4.7 -{\tt print_syntax} displays the sets of names associated with the translation
     4.8 -functions of a theory under \texttt{parse_ast_translation}, etc.  You can add
     4.9 -new ones via the {\tt ML} section\index{*ML section} of a theory definition
    4.10 -file.  There may never be more than one function of the same kind per name.
    4.11 -Even though the {\tt ML} section is the very last part of the file, newly
    4.12 -installed translation functions are already effective when processing all of
    4.13 -the preceding sections.
    4.14 +Function {\tt print_syntax} displays the sets of names associated with the
    4.15 +translation functions of a theory under \texttt{parse_ast_translation}, etc.
    4.16 +You can add new ones via the {\tt ML} section\index{*ML section} of a theory
    4.17 +definition file.  Even though the {\tt ML} section is the very last part of
    4.18 +the file, newly installed translation functions are already effective when
    4.19 +processing all of the preceding sections.
    4.20  
    4.21  The {\tt ML} section's contents are simply copied verbatim near the
    4.22  beginning of the \ML\ file generated from a theory definition file.
    4.23 @@ -757,16 +756,18 @@
    4.24  functions called during the parsing process differ from those for
    4.25  printing more fundamentally in their overall behaviour:
    4.26  \begin{description}
    4.27 -\item[Parse translations] are applied bottom-up.  The arguments are already
    4.28 -  in translated form.  The translations must not fail; exceptions trigger
    4.29 -  an error message.
    4.30 -
    4.31 +\item[Parse translations] are applied bottom-up.  The arguments are already in
    4.32 +  translated form.  The translations must not fail; exceptions trigger an
    4.33 +  error message.  There may never be more than one function associated with
    4.34 +  any syntactic name.
    4.35 +  
    4.36  \item[Print translations] are applied top-down.  They are supplied with
    4.37    arguments that are partly still in internal form.  The result again
    4.38 -  undergoes translation; therefore a print translation should not introduce
    4.39 -  as head the very constant that invoked it.  The function may raise
    4.40 -  exception \xdx{Match} to indicate failure; in this event it has no
    4.41 -  effect.
    4.42 +  undergoes translation; therefore a print translation should not introduce as
    4.43 +  head the very constant that invoked it.  The function may raise exception
    4.44 +  \xdx{Match} to indicate failure; in this event it has no effect.  Multiple
    4.45 +  functions associated with some syntactic name are tried in an unspecified
    4.46 +  order.
    4.47  \end{description}
    4.48  
    4.49  Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
    4.50 @@ -883,22 +884,21 @@
    4.51  example at the end of \S\ref{sec:tr_funs}).
    4.52  
    4.53  \medskip Token translations may be installed by declaring the
    4.54 -\ttindex{token_translation} value within the \texttt{ML} section of a
    4.55 -theory definition file:
    4.56 +\ttindex{token_translation} value within the \texttt{ML} section of a theory
    4.57 +definition file:
    4.58  \begin{ttbox}
    4.59 -val token_translation: (string * string * (string -> string * int)) list
    4.60 +val token_translation: (string * string * (string -> string * real)) list
    4.61  \end{ttbox}\index{token_translation}
    4.62 -The elements of this list are of the form $(m, c, f)$, where $m$ is a
    4.63 -print mode identifier, $c$ a token class, and $f\colon string \to
    4.64 -string \times int$ the actual translation function.  Assuming that $x$
    4.65 -is of identifier class $c$, and print mode $m$ is the first one of all
    4.66 -currently active modes that provide some translation for $c$, then $x$
    4.67 -is output according to $f(x) = (x', len)$.  Thereby $x'$ is the
    4.68 -modified identifier name and $len$ its visual length approximated in
    4.69 -terms of whole characters.  Thus $x'$ may include non-printing parts
    4.70 -like control sequences or markup information for typesetting systems.
    4.71 +The elements of this list are of the form $(m, c, f)$, where $m$ is a print
    4.72 +mode identifier, $c$ a token class, and $f\colon string \to string \times
    4.73 +real$ the actual translation function.  Assuming that $x$ is of identifier
    4.74 +class $c$, and print mode $m$ is the first (active) mode providing some
    4.75 +translation for $c$, then $x$ is output according to $f(x) = (x', len)$.
    4.76 +Thereby $x'$ is the modified identifier name and $len$ its visual length in
    4.77 +terms of characters (e.g.\ length 1.0 would correspond to $1/2$\,em in
    4.78 +\LaTeX).  Thus $x'$ may include non-printing parts like control sequences or
    4.79 +markup information for typesetting systems.
    4.80  
    4.81 -%FIXME example (?)
    4.82  
    4.83  \index{token translations|)}
    4.84