summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 11 Feb 1999 15:30:10 +0100 | |

changeset 6269 | dbb48b0744d3 |

parent 6268 | 9d2dad7489f4 |

child 6270 | c905fe5994a2 |

tuned;
TLA update;

--- a/NEWS Tue Feb 09 10:47:21 1999 +0100 +++ b/NEWS Thu Feb 11 15:30:10 1999 +0100 @@ -1,3 +1,4 @@ + Isabelle NEWS -- history user-relevant changes ============================================== @@ -6,16 +7,17 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** -* HOL: Removed the obsolete syntax "Compl A"; use -A for set complement +* HOL: Removed the obsolete syntax "Compl A"; use -A for set +complement; -* HOL: the predicate "inj" is now defined by translation to "inj_on" +* HOL: the predicate "inj" is now defined by translation to "inj_on"; -* ZF: The con_defs part of an inductive definition may no longer refer to - constants declared in the same theory; +* ZF: The con_defs part of an inductive definition may no longer refer +to constants declared in the same theory; -* HOL, ZF: the function mk_cases, generated by the inductive definition - package, has lost an argument. To simplify its result, it uses the default - simpset instead of a supplied list of theorems. +* HOL, ZF: the function mk_cases, generated by the inductive +definition package, has lost an argument. To simplify its result, it +uses the default simpset instead of a supplied list of theorems. *** Proof tools *** @@ -30,8 +32,8 @@ * in locales, the "assumes" and "defines" parts may be omitted if empty; -* new print_mode "xsymbols" for extended symbol support - (e.g. genuiene long arrows); +* new print_mode "xsymbols" for extended symbol support (e.g. genuine +long arrows); * path element specification '~~' refers to '$ISABELLE_HOME'; @@ -56,6 +58,7 @@ 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)'. + *** Internal programming interfaces *** * tuned current_goals_markers semantics: begin / end goal avoids @@ -66,27 +69,34 @@ uncoditionally; replaced prs_fn by writeln_fn; consider std_output: string -> unit if you really want to output text without newline; +* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization +-- avoids syntactic ambiguities and treats state, transition, and +temporal levels more uniformly; introduces INCOMPATIBILITIES due to +changed syntax and (many) tactics; + *** ZF *** * new primrec section allows primitive recursive functions to be given - directly (as in HOL) over datatypes and the natural numbers; +directly (as in HOL) over datatypes and the natural numbers; -* new tactics induct_tac and exhaust_tac for induction (or case analysis) - over datatypes and the natural numbers; +* new tactics induct_tac and exhaust_tac for induction (or case +analysis) over datatypes and the natural numbers; * the datatype declaration of type T now defines the recursor T_rec; * simplification automatically does freeness reasoning for datatype - constructors; +constructors; -* automatic type-inference, with AddTCs command to insert new type-checking - rules; +* automatic type-inference, with AddTCs command to insert new +type-checking rules; -* datatype introduction rules are now added as Safe Introduction rules to - the claset; +* datatype introduction rules are now added as Safe Introduction rules +to the claset; -* The syntax "if P then x else y" is now available in addition to if(P,x,y). +* the syntax "if P then x else y" is now available in addition to +if(P,x,y); + New in Isabelle98-1 (October 1998)