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