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