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