# HG changeset patch # User paulson # Date 861614368 -7200 # Node ID 223e5d65faaa4e4fda1153b205bea7bdf9f6dcd2 # Parent 8f89a99d2b009cc1ded6b18e54829cb023810277 Reorganized under headings. Also documented Blast_tac and LFilter diff -r 8f89a99d2b00 -r 223e5d65faaa NEWS --- a/NEWS Mon Apr 21 10:38:46 1997 +0200 +++ b/NEWS Mon Apr 21 11:19:28 1997 +0200 @@ -5,10 +5,24 @@ New in Isabelle94-8 (April 1997) -------------------------------- -* reimplemented type inference; +*** General Changes *** + +* new utilities to build / run / maintain Isabelle etc. (in parts +still somewhat experimental); old Makefiles etc. still functional; * INSTALL text, together with ./configure and ./build scripts; +* reimplemented type inference for greater efficiency; + +* prlim command for dealing with lots of subgoals (an easier way of +setting goals_limit); + +*** Syntax + +* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to +be used in conjunction with the Isabelle symbol font; uses the +"symbols" syntax table; + * added token_translation interface (may translate name tokens in arbitrary ways, dependent on their type (free, bound, tfree, ...) and the current print_mode); @@ -16,6 +30,71 @@ * token translations for modes "xterm" and "xterm_color" that display names in bold, underline etc. or colors; +* now supports alternative (named) syntax tables (parser and pretty +printer); internal interface is provided by add_modesyntax(_i); + +* infixes may now be declared with names independent of their syntax; + +* added typed_print_translation (like print_translation, but may +access type of constant); + +*** Classical Reasoner *** + +Blast_tac: a new tactic! It is often more powerful than fast_tac, but has +some limitations. Blast_tac... + + ignores addss, addbefore, addafter; this restriction is intrinsic + + ignores elimination rules that don't have the correct format + (the conclusion MUST be a formula variable) + + ignores types, which can make HOL proofs fail + + rules must not require higher-order unification, e.g. apply_type in ZF + [message "Function Var's argument not a bound variable" relates to this] + + its proof strategy is more general but can actually be slower + +* substitution with equality assumptions no longer permutes other assumptions. + +* minor changes in semantics of addafter (now called addaltern); renamed +setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper +(and access functions for it) + +* improved combination of classical reasoner and simplifier: new +addss, auto_tac, functions for handling clasimpsets, ... Now, the +simplification is safe (therefore moved to safe_step_tac) and thus +more complete, as multiple instantiation of unknowns (with slow_tac). +COULD MAKE EXISTING PROOFS FAIL; in case of problems with +old proofs, use unsafe_addss and unsafe_auto_tac + +*** Simplifier *** + +* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. + +* the solver is now split into a safe and an unsafe part. +This should be invisible for the normal user, except that the +functions setsolver and addsolver have been renamed to setSolver and +addSolver. added safe_asm_full_simp_tac. + +* ordering on terms as parameter (used for ordered rewriting); +added interface for simplification procedures (functions that produce *proven* +rewrite rules on the fly, depending on current redex); + +*** HOL *** + +* patterns in case expressions allow tuple patterns as arguments to +constructors, for example `case x of [] => ... | (x,y,z)#ps => ...' + +* primrec now also works with type nat; + +* the constant for negation has been renamed from "not" to "Not" to +harmonize with FOL, ZF, LK, etc. + +* HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists + +* HOL/ex/Ring.thy declares cring_simp, which solves equational +problems in commutative rings, using axiomatic type classes for + and *; + +* more examples in HOL/MiniML and HOL/Auth; + +* more default rewrite rules for quantifiers, union/intersection; + * HOLCF changes: derived all rules and arities + axiomatic type classes instead of classes + typedef instead of faking type definitions @@ -26,70 +105,12 @@ + eliminated blift from Lift3.thy (use Def instead of blift) all eliminated rules are derived as theorems --> no visible changes -* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. - -* simplifier: the solver is now split into a safe and an unsafe part. -This should be invisible for the normal user, except that the -functions setsolver and addsolver have been renamed to setSolver and -addSolver. added safe_asm_full_simp_tac. - -* classical reasoner: substitution with equality assumptions no longer -permutes other assumptions. - -* classical reasoner: minor changes in semantics of addafter (now called -addaltern); renamed setwrapper to setWrapper and compwrapper to compWrapper; -added safe wrapper (and access functions for it) - -* improved combination of classical reasoner and simplifier: new -addss, auto_tac, functions for handling clasimpsets, ... Now, the -simplification is safe (therefore moved to safe_step_tac) and thus -more complete, as multiple instantiation of unknowns (with slow_tac). -COULD MAKE EXISTING PROOFS FAIL; in case of problems with -old proofs, use unsafe_addss and unsafe_auto_tac - -* HOL: patterns in case expressions allow tuple patterns as arguments to -constructors, for example `case x of [] => ... | (x,y,z)#ps => ...' - -* HOL: primrec now also works with type nat; - -* HOL: the constant for negation has been renamed from "not" to "Not" to -harmonize with FOL, ZF, LK, etc. - -* new utilities to build / run / maintain Isabelle etc. (in parts -still somewhat experimental); old Makefiles etc. still functional; - -* simplifier: termless order as parameter; added interface for -simplification procedures (functions that produce *proven* rewrite -rules on the fly, depending on current redex); - -* now supports alternative (named) syntax tables (parser and pretty -printer); internal interface is provided by add_modesyntax(_i); - -* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to -be used in conjunction with the Isabelle symbol font; uses the -"symbols" syntax table; - -* infixes may now be declared with names independent of their syntax; - -* added typed_print_translation (like print_translation, but may -access type of constant); - -* prlim command for dealing with lots of subgoals (an easier way of -setting goals_limit); - -* HOL/ex/Ring.thy declares cring_simp, which solves equational -problems in commutative rings, using axiomatic type classes for + and *; +*** ZF *** * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default rewrite rule; this may affect some proofs. eq_cs is gone but can be put back as ZF_cs addSIs [equalityI]; -* more examples in HOL/MiniML and HOL/Auth; - -* more default rewrite rules in HOL for quantifiers, union/intersection; - -* the NEWS file; - New in Isabelle94-7 (November 96)