NEWS
author paulson
Wed Jul 28 10:28:08 1999 +0200 (1999-07-28)
changeset 7113 ab79d9fa8d8e
parent 7047 d103b875ef1d
child 7125 df7cf6e85501
permissions -rw-r--r--
LK
     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 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
    11 are no longer simplified.  (This allows the simplifier to unfold recursive
    12 functional programs.)  To restore the old behaviour, declare
    13 	Delcongs [if_weak_cong];
    14 
    15 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
    16 complement;
    17 
    18 * HOL: the predicate "inj" is now defined by translation to "inj_on";
    19 
    20 * HOL/typedef: fixed type inference for representing set; type
    21 arguments now have to occur explicitly on the rhs as type constraints;
    22 
    23 * ZF: The con_defs part of an inductive definition may no longer refer
    24 to constants declared in the same theory;
    25 
    26 * HOL, ZF: the function mk_cases, generated by the inductive
    27 definition package, has lost an argument.  To simplify its result, it
    28 uses the default simpset instead of a supplied list of theorems.
    29 
    30 
    31 *** Proof tools ***
    32 
    33 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
    34 decision procedure for linear arithmetic. Currently it is used for
    35 types `nat' and `int' in HOL (see below) but can, should and will be
    36 instantiated for other types and logics as well.
    37 
    38 
    39 *** General ***
    40 
    41 * Isabelle manuals now also available as PDF;
    42 
    43 * improved browser info generation: better HTML markup (including
    44 colors), graph views in several sizes; isatool usedir now provides a
    45 proper interface for user theories (via -P option);
    46 
    47 * theory loader rewritten from scratch (may not be fully
    48 bug-compatible); old loadpath variable has been replaced by show_path,
    49 add_path, del_path, reset_path functions; new operations such as
    50 update_thy, touch_thy, remove_thy (see also isatool doc ref);
    51 
    52 * in locales, the "assumes" and "defines" parts may be omitted if
    53 empty;
    54 
    55 * new print_mode "xsymbols" for extended symbol support (e.g. genuine
    56 long arrows);
    57 
    58 * new print_mode "HTML";
    59 
    60 * path element specification '~~' refers to '$ISABELLE_HOME';
    61 
    62 * new flag show_tags controls display of tags of theorems (which are
    63 basically just comments that may be attached by some tools);
    64 
    65 * improved isatool install: option -k creates KDE application icon,
    66 option -p DIR installs standalone binaries;
    67 
    68 * added ML_PLATFORM setting (useful for cross-platform installations);
    69 more robust handling of platform specific ML images for SML/NJ;
    70 
    71 * Isamode 2.6 requires patch to accomodate change of Isabelle font
    72 mode and goal output format:
    73 
    74 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el
    75 244c244
    76 <       (list (isa-getenv "ISABELLE") "-msymbols" logic-name)
    77 ---
    78 >       (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)
    79 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el
    80 181c181
    81 < (defconst proofstate-proofstart-regexp "^Level [0-9]+$"
    82 ---
    83 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"
    84 
    85 
    86 *** HOL ***
    87 
    88 * There are now decision procedures for linear arithmetic over nat and
    89 int:
    90 
    91 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
    92 `+', `-', `Suc', `min', `max' and numerical constants; other subterms
    93 are treated as atomic; subformulae not involving type `nat' or `int'
    94 are ignored; quantified subformulae are ignored unless they are
    95 positive universal or negative existential. The tactic has to be
    96 invoked by hand and can be a little bit slow. In particular, the
    97 running time is exponential in the number of occurrences of `min' and
    98 `max', and `-' on `nat'.
    99 
   100 2. fast_arith_tac is a cut-down version of arith_tac: it only takes
   101 (negated) (in)equalities among the premises and the conclusion into
   102 account (i.e. no compound formulae) and does not know about `min' and
   103 `max', and `-' on `nat'. It is fast and is used automatically by the
   104 simplifier.
   105 
   106 NB: At the moment, these decision procedures do not cope with mixed
   107 nat/int formulae where the two parts interact, such as `m < n ==>
   108 int(m) < int(n)'.
   109 
   110 * Integer division and remainder can now be performed on constant arguments.  
   111 
   112 * Many properties of integer multiplication, division and remainder are now
   113 available.
   114 
   115 * New bounded quantifier syntax (input only):
   116   ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
   117 
   118 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
   119 -- avoids syntactic ambiguities and treats state, transition, and
   120 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
   121 changed syntax and (many) tactics;
   122 
   123 * HOL/datatype: Now also handles arbitrarily branching datatypes
   124   (using function types) such as
   125 
   126   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
   127 
   128 * HOL/typedef: fixed type inference for representing set; type
   129 arguments now have to occur explicitly on the rhs as type constraints;
   130 
   131 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects
   132 comma separated list of theorem names rather than an ML expression;
   133 
   134 * reset HOL_quantifiers by default, i.e. quantifiers are printed as
   135 ALL/EX rather than !/?;
   136 
   137 
   138 *** LK ***
   139 
   140 * the notation <<...>> is now available as a notation for sequences of formulas
   141 
   142 * the simplifier is now installed
   143 
   144 * the axiom system has been generalized (thanks to Soren Heilmann) 
   145 
   146 * the classical reasoner now has a default rule database
   147 
   148 
   149 *** ZF ***
   150 
   151 * new primrec section allows primitive recursive functions to be given
   152 directly (as in HOL) over datatypes and the natural numbers;
   153 
   154 * new tactics induct_tac and exhaust_tac for induction (or case
   155 analysis) over datatypes and the natural numbers;
   156 
   157 * the datatype declaration of type T now defines the recursor T_rec;
   158 
   159 * simplification automatically does freeness reasoning for datatype
   160 constructors;
   161 
   162 * automatic type-inference, with AddTCs command to insert new
   163 type-checking rules;
   164 
   165 * datatype introduction rules are now added as Safe Introduction rules
   166 to the claset;
   167 
   168 * the syntax "if P then x else y" is now available in addition to
   169 if(P,x,y);
   170 
   171 
   172 *** Internal programming interfaces ***
   173 
   174 * AxClass.axclass_tac lost the theory argument;
   175 
   176 * tuned current_goals_markers semantics: begin / end goal avoids
   177 printing empty lines;
   178 
   179 * removed prs and prs_fn hook, which was broken because it did not
   180 include \n in its semantics, forcing writeln to add one
   181 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
   182 string -> unit if you really want to output text without newline;
   183 
   184 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
   185 plain output, interface builders may have to enable 'isabelle_font'
   186 mode to get Isabelle font glyphs as before;
   187 
   188 * refined token_translation interface; INCOMPATIBILITY: output length
   189 now of type real instead of int;
   190 
   191 
   192 
   193 New in Isabelle98-1 (October 1998)
   194 ----------------------------------
   195 
   196 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   197 
   198 * several changes of automated proof tools;
   199 
   200 * HOL: major changes to the inductive and datatype packages, including
   201 some minor incompatibilities of theory syntax;
   202 
   203 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
   204 called `inj_on';
   205 
   206 * HOL: removed duplicate thms in Arith:
   207   less_imp_add_less  should be replaced by  trans_less_add1
   208   le_imp_add_le      should be replaced by  trans_le_add1
   209 
   210 * HOL: unary minus is now overloaded (new type constraints may be
   211 required);
   212 
   213 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
   214 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
   215 now taken as an integer constant.
   216 
   217 * Pure: ML function 'theory_of' renamed to 'theory';
   218 
   219 
   220 *** Proof tools ***
   221 
   222 * Simplifier:
   223   1. Asm_full_simp_tac is now more aggressive.
   224      1. It will sometimes reorient premises if that increases their power to
   225         simplify.
   226      2. It does no longer proceed strictly from left to right but may also
   227         rotate premises to achieve further simplification.
   228      For compatibility reasons there is now Asm_lr_simp_tac which is like the
   229      old Asm_full_simp_tac in that it does not rotate premises.
   230   2. The simplifier now knows a little bit about nat-arithmetic.
   231 
   232 * Classical reasoner: wrapper mechanism for the classical reasoner now
   233 allows for selected deletion of wrappers, by introduction of names for
   234 wrapper functionals.  This implies that addbefore, addSbefore,
   235 addaltern, and addSaltern now take a pair (name, tactic) as argument,
   236 and that adding two tactics with the same name overwrites the first
   237 one (emitting a warning).
   238   type wrapper = (int -> tactic) -> (int -> tactic)
   239   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
   240   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
   241   delWrapper, delSWrapper: claset *  string            -> claset
   242   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
   243 
   244 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
   245 semantics; addbefore now affects only the unsafe part of step_tac
   246 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
   247 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
   248 by Force_tac;
   249 
   250 * Classical reasoner: setwrapper to setWrapper and compwrapper to
   251 compWrapper; added safe wrapper (and access functions for it);
   252 
   253 * HOL/split_all_tac is now much faster and fails if there is nothing
   254 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
   255 and the names of the automatically generated variables have changed.
   256 split_all_tac has moved within claset() from unsafe wrappers to safe
   257 wrappers, which means that !!-bound variables are split much more
   258 aggressively, and safe_tac and clarify_tac now split such variables.
   259 If this splitting is not appropriate, use delSWrapper "split_all_tac".
   260 Note: the same holds for record_split_tac, which does the job of
   261 split_all_tac for record fields.
   262 
   263 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
   264 permanently to the default simpset using Addsplits just like
   265 Addsimps. They can be removed via Delsplits just like
   266 Delsimps. Lower-case versions are also available.
   267 
   268 * HOL/Simplifier: The rule split_if is now part of the default
   269 simpset. This means that the simplifier will eliminate all occurrences
   270 of if-then-else in the conclusion of a goal. To prevent this, you can
   271 either remove split_if completely from the default simpset by
   272 `Delsplits [split_if]' or remove it in a specific call of the
   273 simplifier using `... delsplits [split_if]'.  You can also add/delete
   274 other case splitting rules to/from the default simpset: every datatype
   275 generates suitable rules `split_t_case' and `split_t_case_asm' (where
   276 t is the name of the datatype).
   277 
   278 * Classical reasoner / Simplifier combination: new force_tac (and
   279 derivatives Force_tac, force) combines rewriting and classical
   280 reasoning (and whatever other tools) similarly to auto_tac, but is
   281 aimed to solve the given subgoal completely.
   282 
   283 
   284 *** General ***
   285 
   286 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
   287 and `goalw': the theory is no longer needed as an explicit argument -
   288 the current theory context is used; assumptions are no longer returned
   289 at the ML-level unless one of them starts with ==> or !!; it is
   290 recommended to convert to these new commands using isatool fixgoal
   291 (backup your sources first!);
   292 
   293 * new top-level commands 'thm' and 'thms' for retrieving theorems from
   294 the current theory context, and 'theory' to lookup stored theories;
   295 
   296 * new theory section 'locale' for declaring constants, assumptions and
   297 definitions that have local scope;
   298 
   299 * new theory section 'nonterminals' for purely syntactic types;
   300 
   301 * new theory section 'setup' for generic ML setup functions
   302 (e.g. package initialization);
   303 
   304 * the distribution now includes Isabelle icons: see
   305 lib/logo/isabelle-{small,tiny}.xpm;
   306 
   307 * isatool install - install binaries with absolute references to
   308 ISABELLE_HOME/bin;
   309 
   310 * isatool logo -- create instances of the Isabelle logo (as EPS);
   311 
   312 * print mode 'emacs' reserved for Isamode;
   313 
   314 * support multiple print (ast) translations per constant name;
   315 
   316 * theorems involving oracles are now printed with a suffixed [!];
   317 
   318 
   319 *** HOL ***
   320 
   321 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
   322 
   323 * HOL/inductive package reorganized and improved: now supports mutual
   324 definitions such as
   325 
   326   inductive EVEN ODD
   327     intrs
   328       null "0 : EVEN"
   329       oddI "n : EVEN ==> Suc n : ODD"
   330       evenI "n : ODD ==> Suc n : EVEN"
   331 
   332 new theorem list "elims" contains an elimination rule for each of the
   333 recursive sets; inductive definitions now handle disjunctive premises
   334 correctly (also ZF);
   335 
   336 INCOMPATIBILITIES: requires Inductive as an ancestor; component
   337 "mutual_induct" no longer exists - the induction rule is always
   338 contained in "induct";
   339 
   340 
   341 * HOL/datatype package re-implemented and greatly improved: now
   342 supports mutually recursive datatypes such as
   343 
   344   datatype
   345     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
   346             | SUM ('a aexp) ('a aexp)
   347             | DIFF ('a aexp) ('a aexp)
   348             | NUM 'a
   349   and
   350     'a bexp = LESS ('a aexp) ('a aexp)
   351             | AND ('a bexp) ('a bexp)
   352             | OR ('a bexp) ('a bexp)
   353 
   354 as well as indirectly recursive datatypes such as
   355 
   356   datatype
   357     ('a, 'b) term = Var 'a
   358                   | App 'b ((('a, 'b) term) list)
   359 
   360 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
   361 induction on mutually / indirectly recursive datatypes.
   362 
   363 Primrec equations are now stored in theory and can be accessed via
   364 <function_name>.simps.
   365 
   366 INCOMPATIBILITIES:
   367 
   368   - Theories using datatypes must now have theory Datatype as an
   369     ancestor.
   370   - The specific <typename>.induct_tac no longer exists - use the
   371     generic induct_tac instead.
   372   - natE has been renamed to nat.exhaust - use exhaust_tac
   373     instead of res_inst_tac ... natE. Note that the variable
   374     names in nat.exhaust differ from the names in natE, this
   375     may cause some "fragile" proofs to fail.
   376   - The theorems split_<typename>_case and split_<typename>_case_asm
   377     have been renamed to <typename>.split and <typename>.split_asm.
   378   - Since default sorts of type variables are now handled correctly,
   379     some datatype definitions may have to be annotated with explicit
   380     sort constraints.
   381   - Primrec definitions no longer require function name and type
   382     of recursive argument.
   383 
   384 Consider using isatool fixdatatype to adapt your theories and proof
   385 scripts to the new package (backup your sources first!).
   386 
   387 
   388 * HOL/record package: considerably improved implementation; now
   389 includes concrete syntax for record types, terms, updates; theorems
   390 for surjective pairing and splitting !!-bound record variables; proof
   391 support is as follows:
   392 
   393   1) standard conversions (selectors or updates applied to record
   394 constructor terms) are part of the standard simpset;
   395 
   396   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
   397 made part of standard simpset and claset via addIffs;
   398 
   399   3) a tactic for record field splitting (record_split_tac) is part of
   400 the standard claset (addSWrapper);
   401 
   402 To get a better idea about these rules you may retrieve them via
   403 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
   404 the name of your record type.
   405 
   406 The split tactic 3) conceptually simplifies by the following rule:
   407 
   408   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
   409 
   410 Thus any record variable that is bound by meta-all will automatically
   411 blow up into some record constructor term, consequently the
   412 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
   413 solve record problems automatically.
   414 
   415 
   416 * reorganized the main HOL image: HOL/Integ and String loaded by
   417 default; theory Main includes everything;
   418 
   419 * automatic simplification of integer sums and comparisons, using cancellation;
   420 
   421 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
   422 
   423 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   424 
   425 * many new identities for unions, intersections, set difference, etc.;
   426 
   427 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
   428 called split_if, split_split, split_sum_case and split_nat_case (to go
   429 with add/delsplits);
   430 
   431 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
   432 (?x::unit) = (); this is made part of the default simpset, which COULD
   433 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
   434 'Delsimprocs [unit_eq_proc];' as last resort); also note that
   435 unit_abs_eta_conv is added in order to counter the effect of
   436 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
   437 %u.f();
   438 
   439 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
   440 makes more sense);
   441 
   442 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   443   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   444   disjointness reasoning but breaking a few old proofs.
   445 
   446 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
   447 to 'converse' from 'inverse' (for compatibility with ZF and some
   448 literature);
   449 
   450 * HOL/recdef can now declare non-recursive functions, with {} supplied as
   451 the well-founded relation;
   452 
   453 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
   454     Compl A.  The "Compl" syntax remains available as input syntax for this
   455     release ONLY.
   456 
   457 * HOL/Update: new theory of function updates:
   458     f(a:=b) == %x. if x=a then b else f x
   459 may also be iterated as in f(a:=b,c:=d,...);
   460 
   461 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
   462 
   463 * HOL/List:
   464   - new function list_update written xs[i:=v] that updates the i-th
   465     list position. May also be iterated as in xs[i:=a,j:=b,...].
   466   - new function `upt' written [i..j(] which generates the list
   467     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
   468     bound write [i..j], which is a shorthand for [i..j+1(].
   469   - new lexicographic orderings and corresponding wellfoundedness theorems.
   470 
   471 * HOL/Arith:
   472   - removed 'pred' (predecessor) function;
   473   - generalized some theorems about n-1;
   474   - many new laws about "div" and "mod";
   475   - new laws about greatest common divisors (see theory ex/Primes);
   476 
   477 * HOL/Relation: renamed the relational operator r^-1 "converse"
   478 instead of "inverse";
   479 
   480 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
   481   of the multiset ordering;
   482 
   483 * directory HOL/Real: a construction of the reals using Dedekind cuts
   484   (not included by default);
   485 
   486 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   487 
   488 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
   489   programs, i.e. different program variables may have different types.
   490 
   491 * calling (stac rew i) now fails if "rew" has no effect on the goal
   492   [previously, this check worked only if the rewrite rule was unconditional]
   493   Now rew can involve either definitions or equalities (either == or =).
   494 
   495 
   496 *** ZF ***
   497 
   498 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
   499   only the theorems proved on ZF.ML;
   500 
   501 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   502   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   503   disjointness reasoning but breaking a few old proofs.
   504 
   505 * ZF/Update: new theory of function updates
   506     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
   507   may also be iterated as in f(a:=b,c:=d,...);
   508 
   509 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
   510 
   511 * calling (stac rew i) now fails if "rew" has no effect on the goal
   512   [previously, this check worked only if the rewrite rule was unconditional]
   513   Now rew can involve either definitions or equalities (either == or =).
   514 
   515 * case_tac provided for compatibility with HOL
   516     (like the old excluded_middle_tac, but with subgoals swapped)
   517 
   518 
   519 *** Internal programming interfaces ***
   520 
   521 * Pure: several new basic modules made available for general use, see
   522 also src/Pure/README;
   523 
   524 * improved the theory data mechanism to support encapsulation (data
   525 kind name replaced by private Object.kind, acting as authorization
   526 key); new type-safe user interface via functor TheoryDataFun; generic
   527 print_data function becomes basically useless;
   528 
   529 * removed global_names compatibility flag -- all theory declarations
   530 are qualified by default;
   531 
   532 * module Pure/Syntax now offers quote / antiquote translation
   533 functions (useful for Hoare logic etc. with implicit dependencies);
   534 see HOL/ex/Antiquote for an example use;
   535 
   536 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
   537 cterm -> thm;
   538 
   539 * new tactical CHANGED_GOAL for checking that a tactic modifies a
   540 subgoal;
   541 
   542 * Display.print_goals function moved to Locale.print_goals;
   543 
   544 * standard print function for goals supports current_goals_markers
   545 variable for marking begin of proof, end of proof, start of goal; the
   546 default is ("", "", ""); setting current_goals_markers := ("<proof>",
   547 "</proof>", "<goal>") causes SGML like tagged proof state printing,
   548 for example;
   549 
   550 
   551 
   552 New in Isabelle98 (January 1998)
   553 --------------------------------
   554 
   555 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   556 
   557 * changed lexical syntax of terms / types: dots made part of long
   558 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
   559 
   560 * simpset (and claset) reference variable replaced by functions
   561 simpset / simpset_ref;
   562 
   563 * no longer supports theory aliases (via merge) and non-trivial
   564 implicit merge of thms' signatures;
   565 
   566 * most internal names of constants changed due to qualified names;
   567 
   568 * changed Pure/Sequence interface (see Pure/seq.ML);
   569 
   570 
   571 *** General Changes ***
   572 
   573 * hierachically structured name spaces (for consts, types, axms, thms
   574 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
   575 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
   576 isatool fixdots ensures space after dots (e.g. "%x. x"); set
   577 long_names for fully qualified output names; NOTE: ML programs
   578 (special tactics, packages etc.) referring to internal names may have
   579 to be adapted to cope with fully qualified names; in case of severe
   580 backward campatibility problems try setting 'global_names' at compile
   581 time to have enrything declared within a flat name space; one may also
   582 fine tune name declarations in theories via the 'global' and 'local'
   583 section;
   584 
   585 * reimplemented the implicit simpset and claset using the new anytype
   586 data filed in signatures; references simpset:simpset ref etc. are
   587 replaced by functions simpset:unit->simpset and
   588 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
   589 to patch your ML files accordingly;
   590 
   591 * HTML output now includes theory graph data for display with Java
   592 applet or isatool browser; data generated automatically via isatool
   593 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
   594 
   595 * defs may now be conditional; improved rewrite_goals_tac to handle
   596 conditional equations;
   597 
   598 * defs now admits additional type arguments, using TYPE('a) syntax;
   599 
   600 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
   601 creates a new theory node; implicit merge of thms' signatures is
   602 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
   603 transfer:theory->thm->thm in (rare) cases;
   604 
   605 * improved handling of draft signatures / theories; draft thms (and
   606 ctyps, cterms) are automatically promoted to real ones;
   607 
   608 * slightly changed interfaces for oracles: admit many per theory, named
   609 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
   610 
   611 * print_goals: optional output of const types (set show_consts and
   612 show_types);
   613 
   614 * improved output of warnings (###) and errors (***);
   615 
   616 * subgoal_tac displays a warning if the new subgoal has type variables;
   617 
   618 * removed old README and Makefiles;
   619 
   620 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
   621 
   622 * removed obsolete init_pps and init_database;
   623 
   624 * deleted the obsolete tactical STATE, which was declared by
   625     fun STATE tacfun st = tacfun st st;
   626 
   627 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
   628 (which abbreviates $HOME);
   629 
   630 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
   631 use isatool fixseq to adapt your ML programs (this works for fully
   632 qualified references to the Sequence structure only!);
   633 
   634 * use_thy no longer requires writable current directory; it always
   635 reloads .ML *and* .thy file, if either one is out of date;
   636 
   637 
   638 *** Classical Reasoner ***
   639 
   640 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
   641 tactics that use classical reasoning to simplify a subgoal without
   642 splitting it into several subgoals;
   643 
   644 * Safe_tac: like safe_tac but uses the default claset;
   645 
   646 
   647 *** Simplifier ***
   648 
   649 * added simplification meta rules:
   650     (asm_)(full_)simplify: simpset -> thm -> thm;
   651 
   652 * simplifier.ML no longer part of Pure -- has to be loaded by object
   653 logics (again);
   654 
   655 * added prems argument to simplification procedures;
   656 
   657 * HOL, FOL, ZF: added infix function `addsplits':
   658   instead of `<simpset> setloop (split_tac <thms>)'
   659   you can simply write `<simpset> addsplits <thms>'
   660 
   661 
   662 *** Syntax ***
   663 
   664 * TYPE('a) syntax for type reflection terms;
   665 
   666 * no longer handles consts with name "" -- declare as 'syntax' instead;
   667 
   668 * pretty printer: changed order of mixfix annotation preference (again!);
   669 
   670 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
   671 
   672 
   673 *** HOL ***
   674 
   675 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
   676   with `addloop' of the simplifier to faciliate case splitting in premises.
   677 
   678 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
   679 
   680 * HOL/Auth: new protocol proofs including some for the Internet
   681   protocol TLS;
   682 
   683 * HOL/Map: new theory of `maps' a la VDM;
   684 
   685 * HOL/simplifier: simplification procedures nat_cancel_sums for
   686 cancelling out common nat summands from =, <, <= (in)equalities, or
   687 differences; simplification procedures nat_cancel_factor for
   688 cancelling common factor from =, <, <= (in)equalities over natural
   689 sums; nat_cancel contains both kinds of procedures, it is installed by
   690 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
   691 
   692 * HOL/simplifier: terms of the form
   693   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
   694   are rewritten to
   695   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
   696   and those of the form
   697   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
   698   are rewritten to
   699   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
   700 
   701 * HOL/datatype
   702   Each datatype `t' now comes with a theorem `split_t_case' of the form
   703 
   704   P(t_case f1 ... fn x) =
   705      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
   706         ...
   707        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
   708      )
   709 
   710   and a theorem `split_t_case_asm' of the form
   711 
   712   P(t_case f1 ... fn x) =
   713     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
   714         ...
   715        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
   716      )
   717   which can be added to a simpset via `addsplits'. The existing theorems
   718   expand_list_case and expand_option_case have been renamed to
   719   split_list_case and split_option_case.
   720 
   721 * HOL/Arithmetic:
   722   - `pred n' is automatically converted to `n-1'.
   723     Users are strongly encouraged not to use `pred' any longer,
   724     because it will disappear altogether at some point.
   725   - Users are strongly encouraged to write "0 < n" rather than
   726     "n ~= 0". Theorems and proof tools have been modified towards this
   727     `standard'.
   728 
   729 * HOL/Lists:
   730   the function "set_of_list" has been renamed "set" (and its theorems too);
   731   the function "nth" now takes its arguments in the reverse order and
   732   has acquired the infix notation "!" as in "xs!n".
   733 
   734 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
   735 
   736 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
   737   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
   738 
   739 * HOL/record: extensible records with schematic structural subtyping
   740 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
   741 still lacks various theorems and concrete record syntax;
   742 
   743 
   744 *** HOLCF ***
   745 
   746 * removed "axioms" and "generated by" sections;
   747 
   748 * replaced "ops" section by extended "consts" section, which is capable of
   749   handling the continuous function space "->" directly;
   750 
   751 * domain package:
   752   . proves theorems immediately and stores them in the theory,
   753   . creates hierachical name space,
   754   . now uses normal mixfix annotations (instead of cinfix...),
   755   . minor changes to some names and values (for consistency),
   756   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
   757   . separator between mutual domain defs: changed "," to "and",
   758   . improved handling of sort constraints;  now they have to
   759     appear on the left-hand side of the equations only;
   760 
   761 * fixed LAM <x,y,zs>.b syntax;
   762 
   763 * added extended adm_tac to simplifier in HOLCF -- can now discharge
   764 adm (%x. P (t x)), where P is chainfinite and t continuous;
   765 
   766 
   767 *** FOL and ZF ***
   768 
   769 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
   770   with `addloop' of the simplifier to faciliate case splitting in premises.
   771 
   772 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
   773 in HOL, they strip ALL and --> from proved theorems;
   774 
   775 
   776 
   777 New in Isabelle94-8 (May 1997)
   778 ------------------------------
   779 
   780 *** General Changes ***
   781 
   782 * new utilities to build / run / maintain Isabelle etc. (in parts
   783 still somewhat experimental); old Makefiles etc. still functional;
   784 
   785 * new 'Isabelle System Manual';
   786 
   787 * INSTALL text, together with ./configure and ./build scripts;
   788 
   789 * reimplemented type inference for greater efficiency, better error
   790 messages and clean internal interface;
   791 
   792 * prlim command for dealing with lots of subgoals (an easier way of
   793 setting goals_limit);
   794 
   795 
   796 *** Syntax ***
   797 
   798 * supports alternative (named) syntax tables (parser and pretty
   799 printer); internal interface is provided by add_modesyntax(_i);
   800 
   801 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
   802 be used in conjunction with the Isabelle symbol font; uses the
   803 "symbols" syntax table;
   804 
   805 * added token_translation interface (may translate name tokens in
   806 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
   807 the current print_mode); IMPORTANT: user print translation functions
   808 are responsible for marking newly introduced bounds
   809 (Syntax.mark_boundT);
   810 
   811 * token translations for modes "xterm" and "xterm_color" that display
   812 names in bold, underline etc. or colors (which requires a color
   813 version of xterm);
   814 
   815 * infixes may now be declared with names independent of their syntax;
   816 
   817 * added typed_print_translation (like print_translation, but may
   818 access type of constant);
   819 
   820 
   821 *** Classical Reasoner ***
   822 
   823 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
   824 some limitations.  Blast_tac...
   825   + ignores addss, addbefore, addafter; this restriction is intrinsic
   826   + ignores elimination rules that don't have the correct format
   827         (the conclusion MUST be a formula variable)
   828   + ignores types, which can make HOL proofs fail
   829   + rules must not require higher-order unification, e.g. apply_type in ZF
   830     [message "Function Var's argument not a bound variable" relates to this]
   831   + its proof strategy is more general but can actually be slower
   832 
   833 * substitution with equality assumptions no longer permutes other
   834 assumptions;
   835 
   836 * minor changes in semantics of addafter (now called addaltern); renamed
   837 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
   838 (and access functions for it);
   839 
   840 * improved combination of classical reasoner and simplifier:
   841   + functions for handling clasimpsets
   842   + improvement of addss: now the simplifier is called _after_ the
   843     safe steps.
   844   + safe variant of addss called addSss: uses safe simplifications
   845     _during_ the safe steps. It is more complete as it allows multiple
   846     instantiations of unknowns (e.g. with slow_tac).
   847 
   848 *** Simplifier ***
   849 
   850 * added interface for simplification procedures (functions that
   851 produce *proven* rewrite rules on the fly, depending on current
   852 redex);
   853 
   854 * ordering on terms as parameter (used for ordered rewriting);
   855 
   856 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
   857 
   858 * the solver is now split into a safe and an unsafe part.
   859 This should be invisible for the normal user, except that the
   860 functions setsolver and addsolver have been renamed to setSolver and
   861 addSolver; added safe_asm_full_simp_tac;
   862 
   863 
   864 *** HOL ***
   865 
   866 * a generic induction tactic `induct_tac' which works for all datatypes and
   867 also for type `nat';
   868 
   869 * a generic case distinction tactic `exhaust_tac' which works for all
   870 datatypes and also for type `nat';
   871 
   872 * each datatype comes with a function `size';
   873 
   874 * patterns in case expressions allow tuple patterns as arguments to
   875 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
   876 
   877 * primrec now also works with type nat;
   878 
   879 * recdef: a new declaration form, allows general recursive functions to be
   880 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
   881 
   882 * the constant for negation has been renamed from "not" to "Not" to
   883 harmonize with FOL, ZF, LK, etc.;
   884 
   885 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   886 infinite lists;
   887 
   888 * HOL/Modelcheck demonstrates invocation of model checker oracle;
   889 
   890 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   891 problems in commutative rings, using axiomatic type classes for + and *;
   892 
   893 * more examples in HOL/MiniML and HOL/Auth;
   894 
   895 * more default rewrite rules for quantifiers, union/intersection;
   896 
   897 * a new constant `arbitrary == @x.False';
   898 
   899 * HOLCF/IOA replaces old HOL/IOA;
   900 
   901 * HOLCF changes: derived all rules and arities
   902   + axiomatic type classes instead of classes
   903   + typedef instead of faking type definitions
   904   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   905   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   906   + eliminated the types void, one, tr
   907   + use unit lift and bool lift (with translations) instead of one and tr
   908   + eliminated blift from Lift3.thy (use Def instead of blift)
   909   all eliminated rules are derived as theorems --> no visible changes ;
   910 
   911 
   912 *** ZF ***
   913 
   914 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
   915 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
   916 as ZF_cs addSIs [equalityI];
   917 
   918 
   919 
   920 New in Isabelle94-7 (November 96)
   921 ---------------------------------
   922 
   923 * allowing negative levels (as offsets) in prlev and choplev;
   924 
   925 * super-linear speedup for large simplifications;
   926 
   927 * FOL, ZF and HOL now use miniscoping: rewriting pushes
   928 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
   929 FAIL); can suppress it using the command Delsimps (ex_simps @
   930 all_simps); De Morgan laws are also now included, by default;
   931 
   932 * improved printing of ==>  :  ~:
   933 
   934 * new object-logic "Sequents" adds linear logic, while replacing LK
   935 and Modal (thanks to Sara Kalvala);
   936 
   937 * HOL/Auth: correctness proofs for authentication protocols;
   938 
   939 * HOL: new auto_tac combines rewriting and classical reasoning (many
   940 examples on HOL/Auth);
   941 
   942 * HOL: new command AddIffs for declaring theorems of the form P=Q to
   943 the rewriter and classical reasoner simultaneously;
   944 
   945 * function uresult no longer returns theorems in "standard" format;
   946 regain previous version by: val uresult = standard o uresult;
   947 
   948 
   949 
   950 New in Isabelle94-6
   951 -------------------
   952 
   953 * oracles -- these establish an interface between Isabelle and trusted
   954 external reasoners, which may deliver results as theorems;
   955 
   956 * proof objects (in particular record all uses of oracles);
   957 
   958 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
   959 
   960 * "constdefs" section in theory files;
   961 
   962 * "primrec" section (HOL) no longer requires names;
   963 
   964 * internal type "tactic" now simply "thm -> thm Sequence.seq";
   965 
   966 
   967 
   968 New in Isabelle94-5
   969 -------------------
   970 
   971 * reduced space requirements;
   972 
   973 * automatic HTML generation from theories;
   974 
   975 * theory files no longer require "..." (quotes) around most types;
   976 
   977 * new examples, including two proofs of the Church-Rosser theorem;
   978 
   979 * non-curried (1994) version of HOL is no longer distributed;
   980 
   981 
   982 
   983 New in Isabelle94-4
   984 -------------------
   985 
   986 * greatly reduced space requirements;
   987 
   988 * theory files (.thy) no longer require \...\ escapes at line breaks;
   989 
   990 * searchable theorem database (see the section "Retrieving theorems" on
   991 page 8 of the Reference Manual);
   992 
   993 * new examples, including Grabczewski's monumental case study of the
   994 Axiom of Choice;
   995 
   996 * The previous version of HOL renamed to Old_HOL;
   997 
   998 * The new version of HOL (previously called CHOL) uses a curried syntax
   999 for functions.  Application looks like f a b instead of f(a,b);
  1000 
  1001 * Mutually recursive inductive definitions finally work in HOL;
  1002 
  1003 * In ZF, pattern-matching on tuples is now available in all abstractions and
  1004 translates to the operator "split";
  1005 
  1006 
  1007 
  1008 New in Isabelle94-3
  1009 -------------------
  1010 
  1011 * new infix operator, addss, allowing the classical reasoner to
  1012 perform simplification at each step of its search.  Example:
  1013         fast_tac (cs addss ss)
  1014 
  1015 * a new logic, CHOL, the same as HOL, but with a curried syntax
  1016 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
  1017 look like (a,b) instead of <a,b>;
  1018 
  1019 * PLEASE NOTE: CHOL will eventually replace HOL!
  1020 
  1021 * In CHOL, pattern-matching on tuples is now available in all abstractions.
  1022 It translates to the operator "split".  A new theory of integers is available;
  1023 
  1024 * In ZF, integer numerals now denote two's-complement binary integers.
  1025 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
  1026 
  1027 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
  1028 of the Axiom of Choice;
  1029 
  1030 
  1031 
  1032 New in Isabelle94-2
  1033 -------------------
  1034 
  1035 * Significantly faster resolution;
  1036 
  1037 * the different sections in a .thy file can now be mixed and repeated
  1038 freely;
  1039 
  1040 * Database of theorems for FOL, HOL and ZF.  New
  1041 commands including qed, qed_goal and bind_thm store theorems in the database.
  1042 
  1043 * Simple database queries: return a named theorem (get_thm) or all theorems of
  1044 a given theory (thms_of), or find out what theory a theorem was proved in
  1045 (theory_of_thm);
  1046 
  1047 * Bugs fixed in the inductive definition and datatype packages;
  1048 
  1049 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
  1050 and HOL_dup_cs obsolete;
  1051 
  1052 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
  1053 have been removed;
  1054 
  1055 * Simpler definition of function space in ZF;
  1056 
  1057 * new results about cardinal and ordinal arithmetic in ZF;
  1058 
  1059 * 'subtype' facility in HOL for introducing new types as subsets of existing
  1060 types;
  1061 
  1062 
  1063 $Id$