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