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

author | wenzelm |

Mon, 05 May 1997 21:18:01 +0200 | |

changeset 3107 | 492a3d5d2b17 |

parent 3106 | 5396e99c02af |

child 3108 | 335efc3f5632 |

tuned;

--- a/NEWS Mon May 05 18:50:26 1997 +0200 +++ b/NEWS Mon May 05 21:18:01 1997 +0200 @@ -33,7 +33,7 @@ names in bold, underline etc. or colors (which requires a color version of xterm); -* now supports alternative (named) syntax tables (parser and pretty +* 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; @@ -54,18 +54,19 @@ [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. +* 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) +(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 +old proofs, use unsafe_addss and unsafe_auto_tac; *** Simplifier *** @@ -76,28 +77,29 @@ * ordering on terms as parameter (used for ordered rewriting); -* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. +* 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. +addSolver; added safe_asm_full_simp_tac; *** HOL *** * a generic induction tactic `induct_tac' which works for all datatypes and -also for type `nat'. +also for type `nat'; * patterns in case expressions allow tuple patterns as arguments to -constructors, for example `case x of [] => ... | (x,y,z)#ps => ...' +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. +harmonize with FOL, ZF, LK, etc.; -* HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists +* 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 *; @@ -106,6 +108,8 @@ * more default rewrite rules for quantifiers, union/intersection; +* HOLCF/IOA replaces old HOL/IOA; + * HOLCF changes: derived all rules and arities + axiomatic type classes instead of classes + typedef instead of faking type definitions @@ -114,7 +118,7 @@ + eliminated the types void, one, tr + use unit lift and bool lift (with translations) instead of one and tr + eliminated blift from Lift3.thy (use Def instead of blift) - all eliminated rules are derived as theorems --> no visible changes + all eliminated rules are derived as theorems --> no visible changes ; *** ZF ***