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