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