NEWS
changeset 3002 223e5d65faaa
parent 2993 9e46778b97ab
child 3006 8a1eb4531fbb
equal deleted inserted replaced
3001:8f89a99d2b00 3002:223e5d65faaa
     3 ================================================
     3 ================================================
     4 
     4 
     5 New in Isabelle94-8 (April 1997)
     5 New in Isabelle94-8 (April 1997)
     6 --------------------------------
     6 --------------------------------
     7 
     7 
     8 * reimplemented type inference;
     8 *** General Changes ***
       
     9 
       
    10 * new utilities to build / run / maintain Isabelle etc. (in parts
       
    11 still somewhat experimental); old Makefiles etc. still functional;
     9 
    12 
    10 * INSTALL text, together with ./configure and ./build scripts;
    13 * INSTALL text, together with ./configure and ./build scripts;
       
    14 
       
    15 * reimplemented type inference for greater efficiency;
       
    16 
       
    17 * prlim command for dealing with lots of subgoals (an easier way of
       
    18 setting goals_limit);
       
    19 
       
    20 *** Syntax
       
    21 
       
    22 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
       
    23 be used in conjunction with the Isabelle symbol font; uses the
       
    24 "symbols" syntax table;
    11 
    25 
    12 * added token_translation interface (may translate name tokens in
    26 * added token_translation interface (may translate name tokens in
    13 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
    27 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
    14 the current print_mode);
    28 the current print_mode);
    15 
    29 
    16 * token translations for modes "xterm" and "xterm_color" that display
    30 * token translations for modes "xterm" and "xterm_color" that display
    17 names in bold, underline etc. or colors;
    31 names in bold, underline etc. or colors;
       
    32 
       
    33 * now supports alternative (named) syntax tables (parser and pretty
       
    34 printer); internal interface is provided by add_modesyntax(_i);
       
    35 
       
    36 * infixes may now be declared with names independent of their syntax;
       
    37 
       
    38 * added typed_print_translation (like print_translation, but may
       
    39 access type of constant);
       
    40 
       
    41 *** Classical Reasoner ***
       
    42 
       
    43 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
       
    44 some limitations.  Blast_tac...
       
    45   + ignores addss, addbefore, addafter; this restriction is intrinsic
       
    46   + ignores elimination rules that don't have the correct format
       
    47 	(the conclusion MUST be a formula variable)
       
    48   + ignores types, which can make HOL proofs fail
       
    49   + rules must not require higher-order unification, e.g. apply_type in ZF
       
    50     [message "Function Var's argument not a bound variable" relates to this]
       
    51   + its proof strategy is more general but can actually be slower
       
    52 
       
    53 * substitution with equality assumptions no longer permutes other assumptions.
       
    54 
       
    55 * minor changes in semantics of addafter (now called addaltern); renamed
       
    56 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
       
    57 (and access functions for it)
       
    58 
       
    59 * improved combination of classical reasoner and simplifier: new
       
    60 addss, auto_tac, functions for handling clasimpsets, ...  Now, the
       
    61 simplification is safe (therefore moved to safe_step_tac) and thus
       
    62 more complete, as multiple instantiation of unknowns (with slow_tac).
       
    63 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
       
    64 old proofs, use unsafe_addss and unsafe_auto_tac
       
    65 
       
    66 *** Simplifier ***
       
    67 
       
    68 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
       
    69 
       
    70 * the solver is now split into a safe and an unsafe part.
       
    71 This should be invisible for the normal user, except that the
       
    72 functions setsolver and addsolver have been renamed to setSolver and
       
    73 addSolver.  added safe_asm_full_simp_tac.
       
    74 
       
    75 * ordering on terms as parameter (used for ordered rewriting);
       
    76 added interface for simplification procedures (functions that produce *proven*
       
    77 rewrite rules on the fly, depending on current redex);
       
    78 
       
    79 *** HOL ***
       
    80 
       
    81 * patterns in case expressions allow tuple patterns as arguments to
       
    82 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
       
    83 
       
    84 * primrec now also works with type nat;
       
    85 
       
    86 * the constant for negation has been renamed from "not" to "Not" to
       
    87 harmonize with FOL, ZF, LK, etc.
       
    88 
       
    89 * HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists
       
    90 
       
    91 * HOL/ex/Ring.thy declares cring_simp, which solves equational
       
    92 problems in commutative rings, using axiomatic type classes for + and *;
       
    93 
       
    94 * more examples in HOL/MiniML and HOL/Auth;
       
    95 
       
    96 * more default rewrite rules for quantifiers, union/intersection;
    18 
    97 
    19 * HOLCF changes: derived all rules and arities 
    98 * HOLCF changes: derived all rules and arities 
    20   + axiomatic type classes instead of classes 
    99   + axiomatic type classes instead of classes 
    21   + typedef instead of faking type definitions
   100   + typedef instead of faking type definitions
    22   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   101   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
    24   + eliminated the types void, one, tr
   103   + eliminated the types void, one, tr
    25   + use unit lift and bool lift (with translations) instead of one and tr
   104   + use unit lift and bool lift (with translations) instead of one and tr
    26   + eliminated blift from Lift3.thy (use Def instead of blift)
   105   + eliminated blift from Lift3.thy (use Def instead of blift)
    27   all eliminated rules are derived as theorems --> no visible changes 
   106   all eliminated rules are derived as theorems --> no visible changes 
    28 
   107 
    29 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
   108 *** ZF ***
    30 
       
    31 * simplifier: the solver is now split into a safe and an unsafe part.
       
    32 This should be invisible for the normal user, except that the
       
    33 functions setsolver and addsolver have been renamed to setSolver and
       
    34 addSolver.  added safe_asm_full_simp_tac.
       
    35 
       
    36 * classical reasoner: substitution with equality assumptions no longer
       
    37 permutes other assumptions.
       
    38 
       
    39 * classical reasoner: minor changes in semantics of addafter (now called
       
    40 addaltern); renamed setwrapper to setWrapper and compwrapper to compWrapper;
       
    41 added safe wrapper (and access functions for it)
       
    42 
       
    43 * improved combination of classical reasoner and simplifier: new
       
    44 addss, auto_tac, functions for handling clasimpsets, ...  Now, the
       
    45 simplification is safe (therefore moved to safe_step_tac) and thus
       
    46 more complete, as multiple instantiation of unknowns (with slow_tac).
       
    47 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
       
    48 old proofs, use unsafe_addss and unsafe_auto_tac
       
    49 
       
    50 * HOL: patterns in case expressions allow tuple patterns as arguments to
       
    51 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
       
    52 
       
    53 * HOL: primrec now also works with type nat;
       
    54 
       
    55 * HOL: the constant for negation has been renamed from "not" to "Not" to
       
    56 harmonize with FOL, ZF, LK, etc.
       
    57 
       
    58 * new utilities to build / run / maintain Isabelle etc. (in parts
       
    59 still somewhat experimental); old Makefiles etc. still functional;
       
    60 
       
    61 * simplifier: termless order as parameter; added interface for
       
    62 simplification procedures (functions that produce *proven* rewrite
       
    63 rules on the fly, depending on current redex);
       
    64 
       
    65 * now supports alternative (named) syntax tables (parser and pretty
       
    66 printer); internal interface is provided by add_modesyntax(_i);
       
    67 
       
    68 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
       
    69 be used in conjunction with the Isabelle symbol font; uses the
       
    70 "symbols" syntax table;
       
    71 
       
    72 * infixes may now be declared with names independent of their syntax;
       
    73 
       
    74 * added typed_print_translation (like print_translation, but may
       
    75 access type of constant);
       
    76 
       
    77 * prlim command for dealing with lots of subgoals (an easier way of
       
    78 setting goals_limit);
       
    79 
       
    80 * HOL/ex/Ring.thy declares cring_simp, which solves equational
       
    81 problems in commutative rings, using axiomatic type classes for + and *;
       
    82 
   109 
    83 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
   110 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
    84 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
   111 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
    85 as ZF_cs addSIs [equalityI];
   112 as ZF_cs addSIs [equalityI];
    86 
       
    87 * more examples in HOL/MiniML and HOL/Auth;
       
    88 
       
    89 * more default rewrite rules in HOL for quantifiers, union/intersection;
       
    90 
       
    91 * the NEWS file;
       
    92 
   113 
    93 
   114 
    94 
   115 
    95 New in Isabelle94-7 (November 96)
   116 New in Isabelle94-7 (November 96)
    96 ---------------------------------
   117 ---------------------------------