NEWS
author wenzelm
Thu Aug 27 20:45:57 1998 +0200 (1998-08-27)
changeset 5399 0e3b58479d95
parent 5397 034ed25535b9
child 5407 b450fea6d70c
permissions -rw-r--r--
tuned;
     1 
     2 Isabelle NEWS -- history user-relevant changes
     3 ==============================================
     4 
     5 New in this Isabelle version
     6 ----------------------------
     7 
     8 *** Overview of INCOMPATIBILITIES (see below for more details) ***
     9 
    10 * several changes of proof tools;
    11 
    12 * HOL: new version of inductive and datatype;
    13 
    14 * HOL: major changes to the inductive and datatype packages;
    15 
    16 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
    17 called `inj_on';
    18 
    19 * HOL: removed duplicate thms in Arith:
    20   less_imp_add_less  should be replaced by  trans_less_add1
    21   le_imp_add_le      should be replaced by  trans_le_add1
    22 
    23 * Pure: ML function 'theory_of' replaced by 'theory';
    24 
    25 
    26 *** Proof tools ***
    27 
    28 * Simplifier: Asm_full_simp_tac is now more aggressive.
    29   1. It will sometimes reorient premises if that increases their power to
    30      simplify.
    31   2. It does no longer proceed strictly from left to right but may also
    32      rotate premises to achieve further simplification.
    33   For compatibility reasons there is now Asm_lr_simp_tac which is like the
    34   old Asm_full_simp_tac in that it does not rotate premises.
    35 
    36 * Classical reasoner: wrapper mechanism for the classical reasoner now
    37 allows for selected deletion of wrappers, by introduction of names for
    38 wrapper functionals.  This implies that addbefore, addSbefore,
    39 addaltern, and addSaltern now take a pair (name, tactic) as argument,
    40 and that adding two tactics with the same name overwrites the first
    41 one (emitting a warning).
    42   type wrapper = (int -> tactic) -> (int -> tactic)
    43   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
    44   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
    45   delWrapper, delSWrapper: claset *  string            -> claset
    46   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    47 
    48 * HOL/split_all_tac is now much faster and fails if there is nothing
    49 to split.  Existing (fragile) proofs may require adaption because the
    50 order and the names of the automatically generated variables have
    51 changed.  split_all_tac has moved within claset() from unsafe wrappers
    52 to safe wrappers, which means that !!-bound variables are split much
    53 more aggressively, and safe_tac and clarify_tac now split such
    54 variables.  If this splitting is not appropriate, use delSWrapper
    55 "split_all_tac".
    56 
    57 * HOL/Simplifier:
    58 
    59  - Rewrite rules for case distinctions can now be added permanently to
    60    the default simpset using Addsplits just like Addsimps. They can be
    61    removed via Delsplits just like Delsimps. Lower-case versions are
    62    also available.
    63 
    64  - The rule split_if is now part of the default simpset. This means
    65    that the simplifier will eliminate all occurrences of if-then-else
    66    in the conclusion of a goal. To prevent this, you can either remove
    67    split_if completely from the default simpset by `Delsplits
    68    [split_if]' or remove it in a specific call of the simplifier using
    69    `... delsplits [split_if]'.  You can also add/delete other case
    70    splitting rules to/from the default simpset: every datatype
    71    generates suitable rules `split_t_case' and `split_t_case_asm'
    72    (where t is the name of the datatype).
    73 
    74 * Classical reasoner - Simplifier combination: new force_tac (and
    75 derivatives Force_tac, force) combines rewriting and classical
    76 reasoning (and whatever other tools) similarly to auto_tac, but is
    77 aimed to solve the given subgoal completely;
    78 
    79 
    80 *** General ***
    81 
    82 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
    83 and `goalw': the theory is no longer needed as an explicit argument -
    84 the current theory context is used; assumptions are no longer returned
    85 at the ML-level unless one of them starts with ==> or !!; it is
    86 recommended to convert to these new commands using isatool fixgoal
    87 (backup your sources first!);
    88 
    89 * new top-level commands 'thm' and 'thms' for retrieving theorems from
    90 the current theory context, and 'theory' to lookup stored theories;
    91 
    92 * new theory section 'nonterminals' for purely syntactic types;
    93 
    94 * new theory section 'setup' for generic ML setup functions
    95 (e.g. package initialization);
    96 
    97 * the distribution now includes Isabelle icons: see
    98 lib/logo/isabelle-{small,tiny}.xpm;
    99 
   100 * isatool install - install binaries with absolute references to
   101 ISABELLE_HOME/bin;
   102 
   103 
   104 *** HOL ***
   105 
   106 * HOL/inductive package reorganized and improved: now supports mutual
   107 definitions such as
   108 
   109   inductive EVEN ODD
   110     intrs
   111       null "0 : EVEN"
   112       oddI "n : EVEN ==> Suc n : ODD"
   113       evenI "n : ODD ==> Suc n : EVEN"
   114 
   115 new theorem list "elims" contains an elimination rule for each of the
   116 recursive sets; inductive definitions now handle disjunctive premises
   117 correctly (also ZF);
   118 
   119 INCOMPATIBILITIES: requires Inductive as an ancestor; component
   120 "mutual_induct" no longer exists - the induction rule is always
   121 contained in "induct";
   122 
   123 
   124 * HOL/datatype package re-implemented and greatly improved: now
   125 supports mutually recursive datatypes such as
   126 
   127   datatype
   128     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
   129             | SUM ('a aexp) ('a aexp)
   130             | DIFF ('a aexp) ('a aexp)
   131             | NUM 'a
   132   and
   133     'a bexp = LESS ('a aexp) ('a aexp)
   134             | AND ('a bexp) ('a bexp)
   135             | OR ('a bexp) ('a bexp)
   136 
   137 as well as indirectly recursive datatypes such as
   138 
   139   datatype
   140     ('a, 'b) term = Var 'a
   141                   | App 'b ((('a, 'b) term) list)
   142 
   143 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
   144 induction on mutually / indirectly recursive datatypes.
   145 
   146 Primrec equations are now stored in theory and can be accessed via
   147 <function_name>.simps.
   148 
   149 INCOMPATIBILITIES:
   150 
   151   - Theories using datatypes must now have theory Datatype as an
   152     ancestor.
   153   - The specific <typename>.induct_tac no longer exists - use the
   154     generic induct_tac instead.
   155   - natE has been renamed to nat.exhaust - use exhaust_tac
   156     instead of res_inst_tac ... natE. Note that the variable
   157     names in nat.exhaust differ from the names in natE, this
   158     may cause some "fragile" proofs to fail.
   159   - The theorems split_<typename>_case and split_<typename>_case_asm
   160     have been renamed to <typename>.split and <typename>.split_asm.
   161   - Since default sorts of type variables are now handled correctly,
   162     some datatype definitions may have to be annotated with explicit
   163     sort constraints.
   164   - Primrec definitions no longer require function name and type
   165     of recursive argument.
   166 
   167 Consider using isatool fixdatatype to adapt your theories and proof
   168 scripts to the new package (backup your sources first!).
   169 
   170 
   171 * HOL/record package: now includes concrete syntax for record types,
   172 terms, updates; still lacks important theorems, like surjective
   173 pairing and split;
   174 
   175 * reorganized the main HOL image: HOL/Integ and String loaded by
   176 default; theory Main includes everything;
   177 
   178 * added option_map_eq_Some to the default simpset claset;
   179 
   180 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   181 
   182 * many new identities for unions, intersections, set difference, etc.;
   183 
   184 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
   185 called split_if, split_split, split_sum_case and split_nat_case (to go
   186 with add/delsplits);
   187 
   188 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
   189 (?x::unit) = (); this is made part of the default simpset, which COULD
   190 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
   191 'Delsimprocs [unit_eq_proc];' as last resort); also note that
   192 unit_abs_eta_conv is added in order to counter the effect of
   193 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
   194 %u.f();
   195 
   196 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
   197 makes more sense);
   198 
   199 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name was misleading);
   200 
   201 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
   202 to 'converse' from 'inverse' (for compatibility with ZF and some
   203 literature);
   204 
   205 * HOL/recdef can now declare non-recursive functions, with {} supplied as
   206 the well-founded relation;
   207 
   208 * HOL/Update: new theory of function updates:
   209     f(a:=b) == %x. if x=a then b else f x
   210 may also be iterated as in f(a:=b,c:=d,...);
   211 
   212 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
   213 
   214 * HOL/List:
   215   - new function list_update written xs[i:=v] that updates the i-th
   216     list position. May also be iterated as in xs[i:=a,j:=b,...].
   217   - new lexicographic orderings and corresponding wellfoundedness theorems.
   218 
   219 * HOL/Arith:
   220   - removed 'pred' (predecessor) function;
   221   - generalized some theorems about n-1;
   222   - many new laws about "div" and "mod";
   223   - new laws about greatest common divisors (see theory ex/Primes);
   224 
   225 * HOL/Relation: renamed the relational operator r^-1 "converse"
   226 instead of "inverse";
   227 
   228 * directory HOL/Real: a construction of the reals using Dedekind cuts
   229 (not included by default);
   230 
   231 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   232 
   233 * calling (stac rew i) now fails if "rew" has no effect on the goal
   234   [previously, this check worked only if the rewrite rule was unconditional]
   235   Now rew can involve either definitions or equalities (either == or =).
   236 
   237 
   238 *** ZF ***
   239 
   240 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
   241   only the theorems proved on ZF.ML;
   242 
   243 * ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
   244   was misleading).  The rule and 'sym RS equals0E' are now in the default
   245   claset, giving automatic disjointness reasoning but breaking a few old 
   246   proofs.
   247 
   248 * ZF/Update: new theory of function updates
   249     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
   250   may also be iterated as in f(a:=b,c:=d,...);
   251 
   252 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
   253 
   254 * calling (stac rew i) now fails if "rew" has no effect on the goal
   255   [previously, this check worked only if the rewrite rule was unconditional]
   256   Now rew can involve either definitions or equalities (either == or =).
   257 
   258 * case_tac provided for compatibility with HOL
   259     (like the old excluded_middle_tac, but with subgoals swapped)
   260 
   261 
   262 *** Internal programming interfaces ***
   263 
   264 * Pure: several new basic modules made available for general use, see
   265 also src/Pure/README;
   266 
   267 * improved the theory data mechanism to support encapsulation (data
   268 kind name replaced by private Object.kind, acting as authorization
   269 key); new type-safe user interface via functor TheoryDataFun; generic
   270 print_data function becomes basically useless;
   271 
   272 * removed global_names compatibility flag -- all theory declarations
   273 are qualified by default;
   274 
   275 * module Pure/Syntax now offers quote / antiquote translation
   276 functions (useful for Hoare logic etc. with implicit dependencies);
   277 see HOL/ex/Antiquote for an example use;
   278 
   279 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
   280 cterm -> thm;
   281 
   282 * new tactical CHANGED_GOAL for checking that a tactic modifies a
   283 subgoal;
   284 
   285 * Display.print_goals function moved to Locale.print_goals;
   286 
   287 
   288 
   289 New in Isabelle98 (January 1998)
   290 --------------------------------
   291 
   292 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   293 
   294 * changed lexical syntax of terms / types: dots made part of long
   295 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
   296 
   297 * simpset (and claset) reference variable replaced by functions
   298 simpset / simpset_ref;
   299 
   300 * no longer supports theory aliases (via merge) and non-trivial
   301 implicit merge of thms' signatures;
   302 
   303 * most internal names of constants changed due to qualified names;
   304 
   305 * changed Pure/Sequence interface (see Pure/seq.ML);
   306 
   307 
   308 *** General Changes ***
   309 
   310 * hierachically structured name spaces (for consts, types, axms, thms
   311 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
   312 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
   313 isatool fixdots ensures space after dots (e.g. "%x. x"); set
   314 long_names for fully qualified output names; NOTE: ML programs
   315 (special tactics, packages etc.) referring to internal names may have
   316 to be adapted to cope with fully qualified names; in case of severe
   317 backward campatibility problems try setting 'global_names' at compile
   318 time to have enrything declared within a flat name space; one may also
   319 fine tune name declarations in theories via the 'global' and 'local'
   320 section;
   321 
   322 * reimplemented the implicit simpset and claset using the new anytype
   323 data filed in signatures; references simpset:simpset ref etc. are
   324 replaced by functions simpset:unit->simpset and
   325 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
   326 to patch your ML files accordingly;
   327 
   328 * HTML output now includes theory graph data for display with Java
   329 applet or isatool browser; data generated automatically via isatool
   330 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
   331 
   332 * defs may now be conditional; improved rewrite_goals_tac to handle
   333 conditional equations;
   334 
   335 * defs now admits additional type arguments, using TYPE('a) syntax;
   336 
   337 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
   338 creates a new theory node; implicit merge of thms' signatures is
   339 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
   340 transfer:theory->thm->thm in (rare) cases;
   341 
   342 * improved handling of draft signatures / theories; draft thms (and
   343 ctyps, cterms) are automatically promoted to real ones;
   344 
   345 * slightly changed interfaces for oracles: admit many per theory, named
   346 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
   347 
   348 * print_goals: optional output of const types (set show_consts and
   349 show_types);
   350 
   351 * improved output of warnings (###) and errors (***);
   352 
   353 * subgoal_tac displays a warning if the new subgoal has type variables;
   354 
   355 * removed old README and Makefiles;
   356 
   357 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
   358 
   359 * removed obsolete init_pps and init_database;
   360 
   361 * deleted the obsolete tactical STATE, which was declared by
   362     fun STATE tacfun st = tacfun st st;
   363 
   364 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
   365 (which abbreviates $HOME);
   366 
   367 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
   368 use isatool fixseq to adapt your ML programs (this works for fully
   369 qualified references to the Sequence structure only!);
   370 
   371 * use_thy no longer requires writable current directory; it always
   372 reloads .ML *and* .thy file, if either one is out of date;
   373 
   374 
   375 *** Classical Reasoner ***
   376 
   377 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
   378 tactics that use classical reasoning to simplify a subgoal without
   379 splitting it into several subgoals;
   380 
   381 * Safe_tac: like safe_tac but uses the default claset;
   382 
   383 
   384 *** Simplifier ***
   385 
   386 * added simplification meta rules:
   387     (asm_)(full_)simplify: simpset -> thm -> thm;
   388 
   389 * simplifier.ML no longer part of Pure -- has to be loaded by object
   390 logics (again);
   391 
   392 * added prems argument to simplification procedures;
   393 
   394 * HOL, FOL, ZF: added infix function `addsplits':
   395   instead of `<simpset> setloop (split_tac <thms>)'
   396   you can simply write `<simpset> addsplits <thms>'
   397 
   398 
   399 *** Syntax ***
   400 
   401 * TYPE('a) syntax for type reflection terms;
   402 
   403 * no longer handles consts with name "" -- declare as 'syntax' instead;
   404 
   405 * pretty printer: changed order of mixfix annotation preference (again!);
   406 
   407 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
   408 
   409 
   410 *** HOL ***
   411 
   412 * HOL: there is a new splitter `split_asm_tac' that can be used e.g. 
   413   with `addloop' of the simplifier to faciliate case splitting in premises.
   414 
   415 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
   416 
   417 * HOL/Auth: new protocol proofs including some for the Internet
   418   protocol TLS;
   419 
   420 * HOL/Map: new theory of `maps' a la VDM;
   421 
   422 * HOL/simplifier: simplification procedures nat_cancel_sums for
   423 cancelling out common nat summands from =, <, <= (in)equalities, or
   424 differences; simplification procedures nat_cancel_factor for
   425 cancelling common factor from =, <, <= (in)equalities over natural
   426 sums; nat_cancel contains both kinds of procedures, it is installed by
   427 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
   428 
   429 * HOL/simplifier: terms of the form
   430   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
   431   are rewritten to
   432   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
   433   and those of the form
   434   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
   435   are rewritten to
   436   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
   437 
   438 * HOL/datatype
   439   Each datatype `t' now comes with a theorem `split_t_case' of the form
   440 
   441   P(t_case f1 ... fn x) =
   442      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
   443         ...
   444        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
   445      )
   446 
   447   and a theorem `split_t_case_asm' of the form
   448 
   449   P(t_case f1 ... fn x) =
   450     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
   451         ...
   452        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
   453      )
   454   which can be added to a simpset via `addsplits'. The existing theorems
   455   expand_list_case and expand_option_case have been renamed to
   456   split_list_case and split_option_case.
   457 
   458 * HOL/Arithmetic:
   459   - `pred n' is automatically converted to `n-1'.
   460     Users are strongly encouraged not to use `pred' any longer,
   461     because it will disappear altogether at some point.
   462   - Users are strongly encouraged to write "0 < n" rather than
   463     "n ~= 0". Theorems and proof tools have been modified towards this
   464     `standard'.
   465 
   466 * HOL/Lists:
   467   the function "set_of_list" has been renamed "set" (and its theorems too);
   468   the function "nth" now takes its arguments in the reverse order and
   469   has acquired the infix notation "!" as in "xs!n".
   470 
   471 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
   472 
   473 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
   474   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
   475 
   476 * HOL/record: extensible records with schematic structural subtyping
   477 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
   478 still lacks various theorems and concrete record syntax;
   479 
   480 
   481 *** HOLCF ***
   482 
   483 * removed "axioms" and "generated by" sections;
   484 
   485 * replaced "ops" section by extended "consts" section, which is capable of
   486   handling the continuous function space "->" directly;
   487 
   488 * domain package:
   489   . proves theorems immediately and stores them in the theory,
   490   . creates hierachical name space,
   491   . now uses normal mixfix annotations (instead of cinfix...),
   492   . minor changes to some names and values (for consistency),
   493   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
   494   . separator between mutual domain defs: changed "," to "and",
   495   . improved handling of sort constraints;  now they have to
   496     appear on the left-hand side of the equations only;
   497 
   498 * fixed LAM <x,y,zs>.b syntax;
   499 
   500 * added extended adm_tac to simplifier in HOLCF -- can now discharge
   501 adm (%x. P (t x)), where P is chainfinite and t continuous;
   502 
   503 
   504 *** FOL and ZF ***
   505 
   506 * FOL: there is a new splitter `split_asm_tac' that can be used e.g. 
   507   with `addloop' of the simplifier to faciliate case splitting in premises.
   508 
   509 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
   510 in HOL, they strip ALL and --> from proved theorems;
   511 
   512 
   513 
   514 New in Isabelle94-8 (May 1997)
   515 ------------------------------
   516 
   517 *** General Changes ***
   518 
   519 * new utilities to build / run / maintain Isabelle etc. (in parts
   520 still somewhat experimental); old Makefiles etc. still functional;
   521 
   522 * new 'Isabelle System Manual';
   523 
   524 * INSTALL text, together with ./configure and ./build scripts;
   525 
   526 * reimplemented type inference for greater efficiency, better error
   527 messages and clean internal interface;
   528 
   529 * prlim command for dealing with lots of subgoals (an easier way of
   530 setting goals_limit);
   531 
   532 
   533 *** Syntax ***
   534 
   535 * supports alternative (named) syntax tables (parser and pretty
   536 printer); internal interface is provided by add_modesyntax(_i);
   537 
   538 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
   539 be used in conjunction with the Isabelle symbol font; uses the
   540 "symbols" syntax table;
   541 
   542 * added token_translation interface (may translate name tokens in
   543 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
   544 the current print_mode); IMPORTANT: user print translation functions
   545 are responsible for marking newly introduced bounds
   546 (Syntax.mark_boundT);
   547 
   548 * token translations for modes "xterm" and "xterm_color" that display
   549 names in bold, underline etc. or colors (which requires a color
   550 version of xterm);
   551 
   552 * infixes may now be declared with names independent of their syntax;
   553 
   554 * added typed_print_translation (like print_translation, but may
   555 access type of constant);
   556 
   557 
   558 *** Classical Reasoner ***
   559 
   560 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
   561 some limitations.  Blast_tac...
   562   + ignores addss, addbefore, addafter; this restriction is intrinsic
   563   + ignores elimination rules that don't have the correct format
   564 	(the conclusion MUST be a formula variable)
   565   + ignores types, which can make HOL proofs fail
   566   + rules must not require higher-order unification, e.g. apply_type in ZF
   567     [message "Function Var's argument not a bound variable" relates to this]
   568   + its proof strategy is more general but can actually be slower
   569 
   570 * substitution with equality assumptions no longer permutes other
   571 assumptions;
   572 
   573 * minor changes in semantics of addafter (now called addaltern); renamed
   574 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
   575 (and access functions for it);
   576 
   577 * improved combination of classical reasoner and simplifier: 
   578   + functions for handling clasimpsets
   579   + improvement of addss: now the simplifier is called _after_ the
   580     safe steps.
   581   + safe variant of addss called addSss: uses safe simplifications
   582     _during_ the safe steps. It is more complete as it allows multiple 
   583     instantiations of unknowns (e.g. with slow_tac).
   584 
   585 *** Simplifier ***
   586 
   587 * added interface for simplification procedures (functions that
   588 produce *proven* rewrite rules on the fly, depending on current
   589 redex);
   590 
   591 * ordering on terms as parameter (used for ordered rewriting);
   592 
   593 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
   594 
   595 * the solver is now split into a safe and an unsafe part.
   596 This should be invisible for the normal user, except that the
   597 functions setsolver and addsolver have been renamed to setSolver and
   598 addSolver; added safe_asm_full_simp_tac;
   599 
   600 
   601 *** HOL ***
   602 
   603 * a generic induction tactic `induct_tac' which works for all datatypes and
   604 also for type `nat';
   605 
   606 * a generic case distinction tactic `exhaust_tac' which works for all
   607 datatypes and also for type `nat';
   608 
   609 * each datatype comes with a function `size';
   610 
   611 * patterns in case expressions allow tuple patterns as arguments to
   612 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
   613 
   614 * primrec now also works with type nat;
   615 
   616 * recdef: a new declaration form, allows general recursive functions to be
   617 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
   618 
   619 * the constant for negation has been renamed from "not" to "Not" to
   620 harmonize with FOL, ZF, LK, etc.;
   621 
   622 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   623 infinite lists;
   624 
   625 * HOL/Modelcheck demonstrates invocation of model checker oracle;
   626 
   627 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   628 problems in commutative rings, using axiomatic type classes for + and *;
   629 
   630 * more examples in HOL/MiniML and HOL/Auth;
   631 
   632 * more default rewrite rules for quantifiers, union/intersection;
   633 
   634 * a new constant `arbitrary == @x.False';
   635 
   636 * HOLCF/IOA replaces old HOL/IOA;
   637 
   638 * HOLCF changes: derived all rules and arities 
   639   + axiomatic type classes instead of classes 
   640   + typedef instead of faking type definitions
   641   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   642   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   643   + eliminated the types void, one, tr
   644   + use unit lift and bool lift (with translations) instead of one and tr
   645   + eliminated blift from Lift3.thy (use Def instead of blift)
   646   all eliminated rules are derived as theorems --> no visible changes ;
   647 
   648 
   649 *** ZF ***
   650 
   651 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
   652 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
   653 as ZF_cs addSIs [equalityI];
   654 
   655 
   656 
   657 New in Isabelle94-7 (November 96)
   658 ---------------------------------
   659 
   660 * allowing negative levels (as offsets) in prlev and choplev;
   661 
   662 * super-linear speedup for large simplifications;
   663 
   664 * FOL, ZF and HOL now use miniscoping: rewriting pushes
   665 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
   666 FAIL); can suppress it using the command Delsimps (ex_simps @
   667 all_simps); De Morgan laws are also now included, by default;
   668 
   669 * improved printing of ==>  :  ~:
   670 
   671 * new object-logic "Sequents" adds linear logic, while replacing LK
   672 and Modal (thanks to Sara Kalvala);
   673 
   674 * HOL/Auth: correctness proofs for authentication protocols;
   675 
   676 * HOL: new auto_tac combines rewriting and classical reasoning (many
   677 examples on HOL/Auth);
   678 
   679 * HOL: new command AddIffs for declaring theorems of the form P=Q to
   680 the rewriter and classical reasoner simultaneously;
   681 
   682 * function uresult no longer returns theorems in "standard" format;
   683 regain previous version by: val uresult = standard o uresult;
   684 
   685 
   686 
   687 New in Isabelle94-6
   688 -------------------
   689 
   690 * oracles -- these establish an interface between Isabelle and trusted
   691 external reasoners, which may deliver results as theorems;
   692 
   693 * proof objects (in particular record all uses of oracles);
   694 
   695 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
   696 
   697 * "constdefs" section in theory files;
   698 
   699 * "primrec" section (HOL) no longer requires names;
   700 
   701 * internal type "tactic" now simply "thm -> thm Sequence.seq";
   702 
   703 
   704 
   705 New in Isabelle94-5
   706 -------------------
   707 
   708 * reduced space requirements;
   709 
   710 * automatic HTML generation from theories;
   711 
   712 * theory files no longer require "..." (quotes) around most types;
   713 
   714 * new examples, including two proofs of the Church-Rosser theorem;
   715 
   716 * non-curried (1994) version of HOL is no longer distributed;
   717 
   718 
   719 
   720 New in Isabelle94-4
   721 -------------------
   722 
   723 * greatly reduced space requirements;
   724 
   725 * theory files (.thy) no longer require \...\ escapes at line breaks;
   726 
   727 * searchable theorem database (see the section "Retrieving theorems" on 
   728 page 8 of the Reference Manual);
   729 
   730 * new examples, including Grabczewski's monumental case study of the
   731 Axiom of Choice;
   732 
   733 * The previous version of HOL renamed to Old_HOL;
   734 
   735 * The new version of HOL (previously called CHOL) uses a curried syntax 
   736 for functions.  Application looks like f a b instead of f(a,b);
   737 
   738 * Mutually recursive inductive definitions finally work in HOL;
   739 
   740 * In ZF, pattern-matching on tuples is now available in all abstractions and
   741 translates to the operator "split";
   742 
   743 
   744 
   745 New in Isabelle94-3
   746 -------------------
   747 
   748 * new infix operator, addss, allowing the classical reasoner to 
   749 perform simplification at each step of its search.  Example:
   750 	fast_tac (cs addss ss)
   751 
   752 * a new logic, CHOL, the same as HOL, but with a curried syntax 
   753 for functions.  Application looks like f a b instead of f(a,b).  Also pairs 
   754 look like (a,b) instead of <a,b>;
   755 
   756 * PLEASE NOTE: CHOL will eventually replace HOL!
   757 
   758 * In CHOL, pattern-matching on tuples is now available in all abstractions.
   759 It translates to the operator "split".  A new theory of integers is available;
   760 
   761 * In ZF, integer numerals now denote two's-complement binary integers.
   762 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
   763 
   764 * Many new examples: I/O automata, Church-Rosser theorem, equivalents 
   765 of the Axiom of Choice;
   766 
   767 
   768 
   769 New in Isabelle94-2
   770 -------------------
   771 
   772 * Significantly faster resolution;  
   773 
   774 * the different sections in a .thy file can now be mixed and repeated
   775 freely;
   776 
   777 * Database of theorems for FOL, HOL and ZF.  New
   778 commands including qed, qed_goal and bind_thm store theorems in the database.
   779 
   780 * Simple database queries: return a named theorem (get_thm) or all theorems of
   781 a given theory (thms_of), or find out what theory a theorem was proved in
   782 (theory_of_thm);
   783 
   784 * Bugs fixed in the inductive definition and datatype packages;
   785 
   786 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
   787 and HOL_dup_cs obsolete;
   788 
   789 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
   790 have been removed;
   791 
   792 * Simpler definition of function space in ZF;
   793 
   794 * new results about cardinal and ordinal arithmetic in ZF;
   795 
   796 * 'subtype' facility in HOL for introducing new types as subsets of existing
   797 types;
   798 
   799 
   800 $Id$