NEWS
author wenzelm
Wed Jul 09 16:52:51 1997 +0200 (1997-07-09)
changeset 3508 089806e6133b
parent 3454 40b1287347d7
child 3511 da4dd8b7ced4
permissions -rw-r--r--
removed init_database;
     1 
     2 Isabelle NEWS -- history of user-visible changes
     3 ================================================
     4 
     5 New in Isabelle???? (DATE ????)
     6 -------------------------------
     7 
     8 * removed old README and Makefiles;
     9 
    10 
    11 New in Isabelle94-8 (May 1997)
    12 ------------------------------
    13 
    14 *** General Changes ***
    15 
    16 * new utilities to build / run / maintain Isabelle etc. (in parts
    17 still somewhat experimental); old Makefiles etc. still functional;
    18 
    19 * new 'Isabelle System Manual';
    20 
    21 * INSTALL text, together with ./configure and ./build scripts;
    22 
    23 * reimplemented type inference for greater efficiency, better error
    24 messages and clean internal interface;
    25 
    26 * prlim command for dealing with lots of subgoals (an easier way of
    27 setting goals_limit);
    28 
    29 
    30 *** Syntax ***
    31 
    32 * supports alternative (named) syntax tables (parser and pretty
    33 printer); internal interface is provided by add_modesyntax(_i);
    34 
    35 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
    36 be used in conjunction with the Isabelle symbol font; uses the
    37 "symbols" syntax table;
    38 
    39 * added token_translation interface (may translate name tokens in
    40 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
    41 the current print_mode); IMPORTANT: user print translation functions
    42 are responsible for marking newly introduced bounds
    43 (Syntax.mark_boundT);
    44 
    45 * token translations for modes "xterm" and "xterm_color" that display
    46 names in bold, underline etc. or colors (which requires a color
    47 version of xterm);
    48 
    49 * infixes may now be declared with names independent of their syntax;
    50 
    51 * added typed_print_translation (like print_translation, but may
    52 access type of constant);
    53 
    54 
    55 *** Classical Reasoner ***
    56 
    57 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
    58 some limitations.  Blast_tac...
    59   + ignores addss, addbefore, addafter; this restriction is intrinsic
    60   + ignores elimination rules that don't have the correct format
    61 	(the conclusion MUST be a formula variable)
    62   + ignores types, which can make HOL proofs fail
    63   + rules must not require higher-order unification, e.g. apply_type in ZF
    64     [message "Function Var's argument not a bound variable" relates to this]
    65   + its proof strategy is more general but can actually be slower
    66 
    67 * substitution with equality assumptions no longer permutes other
    68 assumptions;
    69 
    70 * minor changes in semantics of addafter (now called addaltern); renamed
    71 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
    72 (and access functions for it);
    73 
    74 * improved combination of classical reasoner and simplifier: 
    75   + functions for handling clasimpsets
    76   + improvement of addss: now the simplifier is called _after_ the
    77     safe steps.
    78   + safe variant of addss called addSss: uses safe simplifications
    79     _during_ the safe steps. It is more complete as it allows multiple 
    80     instantiations of unknowns (e.g. with slow_tac).
    81 
    82 *** Simplifier ***
    83 
    84 * added interface for simplification procedures (functions that
    85 produce *proven* rewrite rules on the fly, depending on current
    86 redex);
    87 
    88 * ordering on terms as parameter (used for ordered rewriting);
    89 
    90 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
    91 
    92 * the solver is now split into a safe and an unsafe part.
    93 This should be invisible for the normal user, except that the
    94 functions setsolver and addsolver have been renamed to setSolver and
    95 addSolver; added safe_asm_full_simp_tac;
    96 
    97 
    98 *** HOL ***
    99 
   100 * a generic induction tactic `induct_tac' which works for all datatypes and
   101 also for type `nat';
   102 
   103 * a generic case distinction tactic `exhaust_tac' which works for all
   104 datatypes and also for type `nat';
   105 
   106 * each datatype comes with a function `size';
   107 
   108 * patterns in case expressions allow tuple patterns as arguments to
   109 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
   110 
   111 * primrec now also works with type nat;
   112 
   113 * recdef: a new declaration form, allows general recursive functions to be
   114 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
   115 
   116 * the constant for negation has been renamed from "not" to "Not" to
   117 harmonize with FOL, ZF, LK, etc.;
   118 
   119 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   120 infinite lists;
   121 
   122 * HOL/Modelcheck demonstrates invocation of model checker oracle;
   123 
   124 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   125 problems in commutative rings, using axiomatic type classes for + and *;
   126 
   127 * more examples in HOL/MiniML and HOL/Auth;
   128 
   129 * more default rewrite rules for quantifiers, union/intersection;
   130 
   131 * a new constant `arbitrary == @x.False';
   132 
   133 * HOLCF/IOA replaces old HOL/IOA;
   134 
   135 * HOLCF changes: derived all rules and arities 
   136   + axiomatic type classes instead of classes 
   137   + typedef instead of faking type definitions
   138   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   139   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   140   + eliminated the types void, one, tr
   141   + use unit lift and bool lift (with translations) instead of one and tr
   142   + eliminated blift from Lift3.thy (use Def instead of blift)
   143   all eliminated rules are derived as theorems --> no visible changes ;
   144 
   145 
   146 *** ZF ***
   147 
   148 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
   149 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
   150 as ZF_cs addSIs [equalityI];
   151 
   152 
   153 
   154 New in Isabelle94-7 (November 96)
   155 ---------------------------------
   156 
   157 * allowing negative levels (as offsets) in prlev and choplev;
   158 
   159 * super-linear speedup for large simplifications;
   160 
   161 * FOL, ZF and HOL now use miniscoping: rewriting pushes
   162 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
   163 FAIL); can suppress it using the command Delsimps (ex_simps @
   164 all_simps); De Morgan laws are also now included, by default;
   165 
   166 * improved printing of ==>  :  ~:
   167 
   168 * new object-logic "Sequents" adds linear logic, while replacing LK
   169 and Modal (thanks to Sara Kalvala);
   170 
   171 * HOL/Auth: correctness proofs for authentication protocols;
   172 
   173 * HOL: new auto_tac combines rewriting and classical reasoning (many
   174 examples on HOL/Auth);
   175 
   176 * HOL: new command AddIffs for declaring theorems of the form P=Q to
   177 the rewriter and classical reasoner simultaneously;
   178 
   179 * function uresult no longer returns theorems in "standard" format;
   180 regain previous version by: val uresult = standard o uresult;
   181 
   182 
   183 
   184 New in Isabelle94-6
   185 -------------------
   186 
   187 * oracles -- these establish an interface between Isabelle and trusted
   188 external reasoners, which may deliver results as theorems;
   189 
   190 * proof objects (in particular record all uses of oracles);
   191 
   192 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
   193 
   194 * "constdefs" section in theory files;
   195 
   196 * "primrec" section (HOL) no longer requires names;
   197 
   198 * internal type "tactic" now simply "thm -> thm Sequence.seq";
   199 
   200 
   201 
   202 New in Isabelle94-5
   203 -------------------
   204 
   205 * reduced space requirements;
   206 
   207 * automatic HTML generation from theories;
   208 
   209 * theory files no longer require "..." (quotes) around most types;
   210 
   211 * new examples, including two proofs of the Church-Rosser theorem;
   212 
   213 * non-curried (1994) version of HOL is no longer distributed;
   214 
   215 
   216 
   217 New in Isabelle94-4
   218 -------------------
   219 
   220 * greatly reduced space requirements;
   221 
   222 * theory files (.thy) no longer require \...\ escapes at line breaks;
   223 
   224 * searchable theorem database (see the section "Retrieving theorems" on 
   225 page 8 of the Reference Manual);
   226 
   227 * new examples, including Grabczewski's monumental case study of the
   228 Axiom of Choice;
   229 
   230 * The previous version of HOL renamed to Old_HOL;
   231 
   232 * The new version of HOL (previously called CHOL) uses a curried syntax 
   233 for functions.  Application looks like f a b instead of f(a,b);
   234 
   235 * Mutually recursive inductive definitions finally work in HOL;
   236 
   237 * In ZF, pattern-matching on tuples is now available in all abstractions and
   238 translates to the operator "split";
   239 
   240 
   241 
   242 New in Isabelle94-3
   243 -------------------
   244 
   245 * new infix operator, addss, allowing the classical reasoner to 
   246 perform simplification at each step of its search.  Example:
   247 	fast_tac (cs addss ss)
   248 
   249 * a new logic, CHOL, the same as HOL, but with a curried syntax 
   250 for functions.  Application looks like f a b instead of f(a,b).  Also pairs 
   251 look like (a,b) instead of <a,b>;
   252 
   253 * PLEASE NOTE: CHOL will eventually replace HOL!
   254 
   255 * In CHOL, pattern-matching on tuples is now available in all abstractions.
   256 It translates to the operator "split".  A new theory of integers is available;
   257 
   258 * In ZF, integer numerals now denote two's-complement binary integers.
   259 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
   260 
   261 * Many new examples: I/O automata, Church-Rosser theorem, equivalents 
   262 of the Axiom of Choice;
   263 
   264 
   265 
   266 New in Isabelle94-2
   267 -------------------
   268 
   269 * Significantly faster resolution;  
   270 
   271 * the different sections in a .thy file can now be mixed and repeated
   272 freely;
   273 
   274 * Database of theorems for FOL, HOL and ZF.  New
   275 commands including qed, qed_goal and bind_thm store theorems in the database.
   276 
   277 * Simple database queries: return a named theorem (get_thm) or all theorems of
   278 a given theory (thms_of), or find out what theory a theorem was proved in
   279 (theory_of_thm);
   280 
   281 * Bugs fixed in the inductive definition and datatype packages;
   282 
   283 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
   284 and HOL_dup_cs obsolete;
   285 
   286 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
   287 have been removed;
   288 
   289 * Simpler definition of function space in ZF;
   290 
   291 * new results about cardinal and ordinal arithmetic in ZF;
   292 
   293 * 'subtype' facility in HOL for introducing new types as subsets of existing
   294 types;
   295 
   296 
   297 $Id$