NEWS
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2756 643cba384a61
child 2773 36fdd908a26c
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
     1 
     2 Isabelle NEWS -- history of user-visible changes
     3 ================================================
     4 
     5 New in Isabelle94-8 (April 1997)
     6 --------------------------------
     7 
     8 * added token_translation interface (may translate name tokens in
     9 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
    10 the current print_mode);
    11 
    12 * token translations for modes "xterm" and "xterm_color" that display
    13 names in bold, underline etc. or colors;
    14 
    15 * HOLCF changes: derived all rules and arities 
    16   + axiomatic type classes instead of classes 
    17   + typedef instead of faking type definitions
    18   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
    19   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
    20   + eliminated the types void, one, tr
    21   + use unit lift and bool lift (with translations) instead of one and tr
    22   + eliminated blift from Lift3.thy (use Def instead of blift)
    23   all eliminated rules are derived as theorems --> no visible changes 
    24 
    25 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
    26 
    27 * simplifier: the solver is now split into a safe and an unsafe part.
    28 This should be invisible for the normal user, except that the
    29 functions setsolver and addsolver have been renamed to setSolver and
    30 addSolver.  added safe_asm_full_simp_tac.
    31 
    32 * classical reasoner: substitution with equality assumptions no longer
    33 permutes other assumptions.
    34 
    35 * classical reasoner: minor changes in semantics of addafter (now called
    36 addaltern); renamed setwrapper to setWrapper and addwrapper to addWrapper;
    37 added safe wrapper (and access functions for it)
    38 
    39 * improved combination of classical reasoner and simplifier: new
    40 addss, auto_tac, functions for handling clasimpsets, ...  Now, the
    41 simplification is safe (therefore moved to safe_step_tac) and thus
    42 more complete, as multiple instantiation of unknowns (with slow_tac).
    43 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
    44 old proofs, use unsafe_addss and unsafe_auto_tac
    45 
    46 * HOL: primrec now also works with type nat;
    47 
    48 * HOL: the constant for negation has been renamed from "not" to "Not" to
    49 harmonize with FOL, ZF, LK, etc.
    50 
    51 * new utilities to build / run / maintain Isabelle etc. (in parts
    52 still somewhat experimental); old Makefiles etc. still functional;
    53 
    54 * simplifier: termless order as parameter; added interface for
    55 simplification procedures (functions that produce *proven* rewrite
    56 rules on the fly, depending on current redex);
    57 
    58 * now supports alternative (named) syntax tables (parser and pretty
    59 printer); internal interface is provided by add_modesyntax(_i);
    60 
    61 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
    62 be used in conjunction with the Isabelle symbol font; uses the
    63 "symbols" syntax table;
    64 
    65 * infixes may now be declared with names independent of their syntax;
    66 
    67 * added typed_print_translation (like print_translation, but may
    68 access type of constant);
    69 
    70 * prlim command for dealing with lots of subgoals (an easier way of
    71 setting goals_limit);
    72 
    73 * HOL/ex/Ring.thy declares cring_simp, which solves equational
    74 problems in commutative rings, using axiomatic type classes for + and *;
    75 
    76 * ZF now has Fast_tac, Simp_tac and Auto_tac.  WARNING: don't use
    77 ZF.thy anymore!  Contains fewer defs and could make a bogus simpset.
    78 Beware of Union_iff.  eq_cs is gone, can be put back as ZF_cs addSIs
    79 [equalityI];
    80 
    81 * more examples in HOL/MiniML and HOL/Auth;
    82 
    83 * more default rewrite rules in HOL for quantifiers, union/intersection;
    84 
    85 * the NEWS file;
    86 
    87 
    88 
    89 New in Isabelle94-7 (November 96)
    90 ---------------------------------
    91 
    92 * allowing negative levels (as offsets) in prlev and choplev;
    93 
    94 * super-linear speedup for large simplifications;
    95 
    96 * FOL, ZF and HOL now use miniscoping: rewriting pushes
    97 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
    98 FAIL); can suppress it using the command Delsimps (ex_simps @
    99 all_simps); De Morgan laws are also now included, by default;
   100 
   101 * improved printing of ==>  :  ~:
   102 
   103 * new object-logic "Sequents" adds linear logic, while replacing LK
   104 and Modal (thanks to Sara Kalvala);
   105 
   106 * HOL/Auth: correctness proofs for authentication protocols;
   107 
   108 * HOL: new auto_tac combines rewriting and classical reasoning (many
   109 examples on HOL/Auth);
   110 
   111 * HOL: new command AddIffs for declaring theorems of the form P=Q to
   112 the rewriter and classical reasoner simultaneously;
   113 
   114 * function uresult no longer returns theorems in "standard" format;
   115 regain previous version by: val uresult = standard o uresult;
   116 
   117 
   118 
   119 New in Isabelle94-6
   120 -------------------
   121 
   122 * oracles -- these establish an interface between Isabelle and trusted
   123 external reasoners, which may deliver results as theorems;
   124 
   125 * proof objects (in particular record all uses of oracles);
   126 
   127 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
   128 
   129 * "constdefs" section in theory files;
   130 
   131 * "primrec" section (HOL) no longer requires names;
   132 
   133 * internal type "tactic" now simply "thm -> thm Sequence.seq";
   134 
   135 
   136 
   137 New in Isabelle94-5
   138 -------------------
   139 
   140 * reduced space requirements;
   141 
   142 * automatic HTML generation from theories;
   143 
   144 * theory files no longer require "..." (quotes) around most types;
   145 
   146 * new examples, including two proofs of the Church-Rosser theorem;
   147 
   148 * non-curried (1994) version of HOL is no longer distributed;
   149 
   150 
   151 
   152 New in Isabelle94-4
   153 -------------------
   154 
   155 * greatly reduced space requirements;
   156 
   157 * theory files (.thy) no longer require \...\ escapes at line breaks;
   158 
   159 * searchable theorem database (see the section "Retrieving theorems" on 
   160 page 8 of the Reference Manual);
   161 
   162 * new examples, including Grabczewski's monumental case study of the
   163 Axiom of Choice;
   164 
   165 * The previous version of HOL renamed to Old_HOL;
   166 
   167 * The new version of HOL (previously called CHOL) uses a curried syntax 
   168 for functions.  Application looks like f a b instead of f(a,b);
   169 
   170 * Mutually recursive inductive definitions finally work in HOL;
   171 
   172 * In ZF, pattern-matching on tuples is now available in all abstractions and
   173 translates to the operator "split";
   174 
   175 
   176 
   177 New in Isabelle94-3
   178 -------------------
   179 
   180 * new infix operator, addss, allowing the classical reasoner to 
   181 perform simplification at each step of its search.  Example:
   182 	fast_tac (cs addss ss)
   183 
   184 * a new logic, CHOL, the same as HOL, but with a curried syntax 
   185 for functions.  Application looks like f a b instead of f(a,b).  Also pairs 
   186 look like (a,b) instead of <a,b>;
   187 
   188 * PLEASE NOTE: CHOL will eventually replace HOL!
   189 
   190 * In CHOL, pattern-matching on tuples is now available in all abstractions.
   191 It translates to the operator "split".  A new theory of integers is available;
   192 
   193 * In ZF, integer numerals now denote two's-complement binary integers.
   194 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
   195 
   196 * Many new examples: I/O automata, Church-Rosser theorem, equivalents 
   197 of the Axiom of Choice;
   198 
   199 
   200 
   201 New in Isabelle94-2
   202 -------------------
   203 
   204 * Significantly faster resolution;  
   205 
   206 * the different sections in a .thy file can now be mixed and repeated
   207 freely;
   208 
   209 * Database of theorems for FOL, HOL and ZF.  New
   210 commands including qed, qed_goal and bind_thm store theorems in the database.
   211 
   212 * Simple database queries: return a named theorem (get_thm) or all theorems of
   213 a given theory (thms_of), or find out what theory a theorem was proved in
   214 (theory_of_thm);
   215 
   216 * Bugs fixed in the inductive definition and datatype packages;
   217 
   218 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
   219 and HOL_dup_cs obsolete;
   220 
   221 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
   222 have been removed;
   223 
   224 * Simpler definition of function space in ZF;
   225 
   226 * new results about cardinal and ordinal arithmetic in ZF;
   227 
   228 * 'subtype' facility in HOL for introducing new types as subsets of existing
   229 types;
   230 
   231 
   232 $Id$