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