wenzelm@2553: wenzelm@2553: Isabelle NEWS -- history of user-visible changes wenzelm@2553: ================================================ wenzelm@2553: wenzelm@2553: New in Isabelle94-8 (???????????) wenzelm@2553: --------------------------------- wenzelm@2553: wenzelm@2553: * the NEWS file; wenzelm@2553: wenzelm@2553: * new utilities to build / run / maintain Isabelle etc. (in parts wenzelm@2553: still somewhat experimental); wenzelm@2553: wenzelm@2553: * simplifier: termless order as parameter; added interface for wenzelm@2553: simplification procedures (functions that produce *proven* rewrite wenzelm@2553: rules on the fly, depending on current redex); wenzelm@2553: wenzelm@2553: * now supports alternative (named) syntax tables (parser and pretty wenzelm@2553: printer); internal interface is provided by add_modesyntax(_i); wenzelm@2553: wenzelm@2553: * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to wenzelm@2553: be used in conjunction with the isabelle symbol font; uses the wenzelm@2553: "symbols" syntax table; wenzelm@2553: wenzelm@2553: * infixes may now be declared with names independent of their syntax; wenzelm@2553: wenzelm@2553: * added typed_print_translation (like print_translation, but also gets wenzelm@2553: the type of the constant); wenzelm@2553: wenzelm@2553: * prlim command for dealing with lots of subgoals (an easier way of wenzelm@2553: setting goals_limit); wenzelm@2553: wenzelm@2553: * HOL/ex/Ring.thy declares cring_simp, which solves equational wenzelm@2553: problems in commutative rings, using axiomatic type classes for + and *; wenzelm@2553: wenzelm@2553: * ZF now has Fast_tac, Simp_tac and Auto_tac. WARNING: don't use wenzelm@2553: ZF.thy anymore! Contains fewer defs and could make a bogus simpset. wenzelm@2553: Beware of Union_iff. eq_cs is gone, can be put back as ZF_cs addSIs wenzelm@2553: [equalityI]; wenzelm@2553: wenzelm@2553: * more examples in HOL/MiniML and HOL/Auth; wenzelm@2553: wenzelm@2553: * more default rewrite rules in HOL for quantifiers, union/intersection; wenzelm@2553: wenzelm@2553: wenzelm@2553: New in Isabelle94-7 (November 96) wenzelm@2553: --------------------------------- wenzelm@2553: wenzelm@2553: * allowing negative levels (as offsets) in prlev and choplev; wenzelm@2553: wenzelm@2553: * many more things we do not remember :-) wenzelm@2553: wenzelm@2553: $Id$