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