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