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