# HG changeset patch # User wenzelm # Date 899484782 -7200 # Node ID ef467e05da61b41aab8fa41617032f3a4b605fc5 # Parent 01cbf154d926d99d2dcb3fbb5b2fecd85f22d20d cleaned up; diff -r 01cbf154d926 -r ef467e05da61 NEWS --- a/NEWS Fri Jul 03 18:05:03 1998 +0200 +++ b/NEWS Fri Jul 03 18:53:02 1998 +0200 @@ -1,17 +1,16 @@ + Isabelle NEWS -- history of user-visible changes ================================================ New in this Isabelle version ---------------------------- -*** General Changes *** +*** Overview of INCOMPATIBILITIES (see below for more details) *** -* new toplevel commands `Goal' and `Goalw' that improve upon `goal' -and `goalw': the theory is no longer needed as an explicit argument - -the current theory is used; assumptions are no longer returned at the -ML-level unless one of them starts with ==> or !!; it is recommended -to convert to these new commands using isatool fixgoal (as usual, -backup your sources first!); +* HOL/inductive requires Inductive.thy as an ancestor; + + +*** Proof tools *** * Simplifier: Asm_full_simp_tac is now more aggressive. 1. It will sometimes reorient premises if that increases their power to @@ -21,27 +20,66 @@ For compatibility reasons there is now Asm_lr_simp_tac which is like the old Asm_full_simp_tac in that it does not rotate premises. -* Changed wrapper mechanism for the classical reasoner now allows for -selected deletion of wrappers, by introduction of names for wrapper -functionals. This implies that addbefore, addSbefore, addaltern, and -addSaltern now take a pair (name, tactic) as argument, and that adding -two tactics with the same name overwrites the first one (emitting a -warning). +* Classical reasoner: wrapper mechanism for the classical reasoner now +allows for selected deletion of wrappers, by introduction of names for +wrapper functionals. This implies that addbefore, addSbefore, +addaltern, and addSaltern now take a pair (name, tactic) as argument, +and that adding two tactics with the same name overwrites the first +one (emitting a warning). type wrapper = (int -> tactic) -> (int -> tactic) setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by addWrapper, addSWrapper: claset * (string * wrapper) -> claset delWrapper, delSWrapper: claset * string -> claset getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; -* inductive definitions now handle disjunctive premises correctly (HOL -and ZF); +* HOL/split_all_tac is now much faster and fails if there is nothing +to split. Existing (fragile) proofs may require adaption because the +order and the names of the automatically generated variables have +changed. split_all_tac has moved within claset() from unsafe wrappers +to safe wrappers, which means that !!-bound variables are split much +more aggressively, and safe_tac and clarify_tac now split such +variables. If this splitting is not appropriate, use delSWrapper +"split_all_tac". + +* HOL/Simplifier: + + - Rewrite rules for case distinctions can now be added permanently to + the default simpset using Addsplits just like Addsimps. They can be + removed via Delsplits just like Delsimps. Lower-case versions are + also available. + + - The rule split_if is now part of the default simpset. This means + that the simplifier will eliminate all occurrences of if-then-else + in the conclusion of a goal. To prevent this, you can either remove + split_if completely from the default simpset by `Delsplits + [split_if]' or remove it in a specific call of the simplifier using + `... delsplits [split_if]'. You can also add/delete other case + splitting rules to/from the default simpset: every datatype + generates suitable rules `split_t_case' and `split_t_case_asm' + (where t is the name of the datatype). + +* Classical reasoner - Simplifier combination: new force_tac (and +derivatives Force_tac, force) combines rewriting and classical +reasoning (and whatever other tools) similarly to auto_tac, but is +aimed to solve the given subgoal completely; + + +*** General *** + +* new toplevel commands `Goal' and `Goalw' that improve upon `goal' +and `goalw': the theory is no longer needed as an explicit argument - +the current theory context is used; assumptions are no longer returned +at the ML-level unless one of them starts with ==> or !!; it is +recommended to convert to these new commands using isatool fixgoal (as +usual, backup your sources first!); * new toplevel commands 'thm' and 'thms' for retrieving theorems from the current theory context; -* new theory section 'nonterminals'; +* new theory section 'nonterminals' for purely syntactic types; -* new theory section 'setup'; +* new theory section 'setup' for generic ML setup functions +(e.g. package initialization); *** HOL *** @@ -49,12 +87,26 @@ * reorganized the main HOL image: HOL/Integ and String loaded by default; theory Main includes everything; -* HOL/Real: a construction of the reals using Dedekind cuts; +* added option_map_eq_Some to the default simpset claset; + +* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset; + +* many new identities for unions, intersections, set difference, etc.; + +* expand_if, expand_split, expand_sum_case and expand_nat_case are now +called split_if, split_split, split_sum_case and split_nat_case (to go +with add/delsplits); -* HOL/record: now includes concrete syntax for record terms (still -lacks important theorems, like surjective pairing and split); +* HOL/Prod introduces simplification procedure unit_eq_proc rewriting +(?x::unit) = (); this is made part of the default simpset, which COULD +MAKE EXISTING PROOFS FAIL under rare circumstances (consider +'Delsimprocs [unit_eq_proc];' as last resort); -* Inductive definition package: Mutually recursive definitions such as +* HOL/record package: now includes concrete syntax for record terms +(still lacks important theorems, like surjective pairing and split); + +* HOL/inductive package reorganized and improved: now supports mutual +definitions such as inductive EVEN ODD intrs @@ -62,79 +114,37 @@ oddI "n : EVEN ==> Suc n : ODD" evenI "n : ODD ==> Suc n : EVEN" - are now possible. Theories containing (co)inductive definitions must now - have theory "Inductive" as an ancestor. The new component "elims" of the - structure created by the package contains an elimination rule for each of - the recursive sets. Note that the component "mutual_induct" no longer - exists - the induction rule is always contained in "induct". - -* simplification procedure unit_eq_proc rewrites (?x::unit) = (); this -is made part of the default simpset of Prod.thy, which COULD MAKE -EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last -resort); +new component "elims" of the structure created by the package contains +an elimination rule for each of the recursive sets; requires +Inductive.thy as an ancestor; component "mutual_induct" no longer +exists - the induction rule is always contained in "induct"; inductive +definitions now handle disjunctive premises correctly (also ZF); -* new force_tac (and its derivations Force_tac, force): combines -rewriting and classical reasoning (and whatever other tools) similarly -to auto_tac, but is aimed to solve the given subgoal totally; - -* added option_map_eq_Some to simpset() and claset(); +* HOL/recdef can now declare non-recursive functions, with {} supplied as +the well-founded relation; -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism; +* HOL/Update: new theory of function updates: + f(a:=b) == %x. if x=a then b else f x +may also be iterated as in f(a:=b,c:=d,...); -* New theory HOL/Update of function updates: - f(a:=b) == %x. if x=a then b else f x - May also be iterated as in f(a:=b,c:=d,...). +* HOL/Vimage: new theory for inverse image of a function, syntax f-``B; * HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...]. -* split_all_tac is now much faster and fails if there is nothing to -split. Existing (fragile) proofs may require adaption because the -order and the names of the automatically generated variables have -changed. split_all_tac has moved within claset() from usafe wrappers -to safe wrappers, which means that !!-bound variables are splitted -much more aggressively, and safe_tac and clarify_tac now split such -variables. If this splitting is not appropriate, use delSWrapper -"split_all_tac". +* HOL/Arith: + - removed 'pred' (predecessor) function; + - generalized some theorems about n-1; + - many new laws about "div" and "mod"; + - new laws about greatest common divisors (see theory ex/Primes); -* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset; - -* HOL/Arithmetic: - - - removed 'pred' (predecessor) function - - generalized some theorems about n-1 - - Many new laws about "div" and "mod" - - New laws about greatest common divisors (see theory ex/Primes) - -* HOL/Relation: renamed the relational operatotr r^-1 "converse" +* HOL/Relation: renamed the relational operator r^-1 "converse" instead of "inverse"; -* recdef can now declare non-recursive functions, with {} supplied as -the well-founded relation; - -* expand_if, expand_split, expand_sum_case and expand_nat_case are now called - split_if, split_split, split_sum_case and split_nat_case - (to go with add/delsplits). - -* Simplifier: - - -Rewrite rules for case distinctions can now be added permanently to the - default simpset using Addsplits just like Addsimps. They can be removed via - Delsplits just like Delsimps. Lower-case versions are also available. +* directory HOL/Real: a construction of the reals using Dedekind cuts +(not included by default); - -The rule split_if is now part of the default simpset. This means that - the simplifier will eliminate all ocurrences of if-then-else in the - conclusion of a goal. To prevent this, you can either remove split_if - completely from the default simpset by `Delsplits [split_if]' or - remove it in a specific call of the simplifier using - `... delsplits [split_if]'. - You can also add/delete other case splitting rules to/from the default - simpset: every datatype generates suitable rules `split_t_case' and - `split_t_case_asm' (where t is the name of the datatype). - -* new theory Vimage (inverse image of a function, syntax f-``B); - -* many new identities for unions, intersections, set difference, etc.; +* directory HOL/UNITY: Chandy and Misra's UNITY formalism; *** ZF *** @@ -142,7 +152,7 @@ * in let x=t in u(x), neither t nor u(x) has to be an FOL term. -*** Internal changes *** +*** Internal programming interfaces *** * improved the theory data mechanism to support encapsulation (data kind name replaced by private Object.kind, acting as authorization @@ -151,6 +161,9 @@ * module Pure/Syntax now offers quote / antiquote translation functions (useful for Hoare logic etc. with implicit dependencies); +* Simplifier now offers conversions (asm_)(full_)rewrite: simpset -> +cterm -> thm; + New in Isabelle98 (January 1998)