NEWS
author wenzelm
Wed May 31 14:30:28 2000 +0200 (2000-05-31)
changeset 9011 0cfc347f8d19
parent 8994 803533fbb3ec
child 9028 8a1ec8f05f14
permissions -rw-r--r--
Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
the current context is now done automatically);
     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: simplification of natural numbers is much changed; to partly
    11 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
    12 issue the following ML commands:
    13 
    14   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
    15   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
    16 
    17 * HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be
    18 needed;
    19 
    20 * HOL: the constant for f``x is now "image" rather than "op ``";
    21 
    22 * HOL: the cartesian product is now "<*>" instead of "Times"; the
    23 lexicographic product is now "<*lex*>" instead of "**";
    24 
    25 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
    26 
    27 * HOL: simplification no longer dives into case-expressions
    28 
    29 * HOL: the recursion equations generated by 'recdef' are now called
    30 f.simps instead of f.rules;
    31 
    32 * HOL: theory Sexp now in HOL/Induct examples (used to be part of main
    33 HOL, but was unused); should better use HOL's datatype package anyway;
    34 
    35 * HOL/Real: "rabs" replaced by overloaded "abs" function;
    36 
    37 * HOL/ML: even fewer consts are declared as global (see theories Ord,
    38 Lfp, Gfp, WF); this only affects ML packages that refer to const names
    39 internally;
    40 
    41 * Isar: changed syntax of local blocks from {{ }} to { };
    42 
    43 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
    44 timing flag supersedes proof_timing and Toplevel.trace;
    45 
    46 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    47 
    48 * LaTeX: several improvements of isabelle.sty;
    49 
    50 
    51 *** Document preparation ***
    52 
    53 * isatool mkdir provides easy setup of Isabelle session directories,
    54 including proper document sources;
    55 
    56 * generated LaTeX sources are now deleted after successful run
    57 (isatool document -c); may retain a copy somewhere else via -D option
    58 of isatool usedir;
    59 
    60 * isatool usedir -D now lets isatool latex -o sty update the Isabelle
    61 style files, achieving self-contained LaTeX sources;
    62 
    63 * old-style theories now produce (crude) LaTeX output as well;
    64 
    65 
    66 *** Isar ***
    67 
    68 * Pure: local results and corresponding term bindings are now subject
    69 to Hindley-Milner polymorphism (similar to ML); this accommodates
    70 incremental type-inference nicely;
    71 
    72 * Pure: new 'obtain' language element supports generalized existence
    73 reasoning;
    74 
    75 * Pure: new calculational elements 'moreover' and 'ultimately' support
    76 plain accumulation of results, without applying any rules yet;
    77 
    78 * Pure: scalable support for case-analysis type proofs: new 'case'
    79 language element refers to local contexts symbolically, as produced by
    80 certain proof methods; internally, case names are attached to theorems
    81 as "tags";
    82 
    83 * Pure: changed syntax of local blocks from {{ }} to { };
    84 
    85 * Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}"
    86 instead of {a, b, c};
    87 
    88 * Pure now provides its own version of intro/elim/dest attributes;
    89 useful for building new logics, but beware of confusion with the
    90 Provers/classical ones;
    91 
    92 * Pure: the local context of (non-atomic) goals is provided via case
    93 name 'antecedent';
    94 
    95 * Pure: removed obsolete 'transfer' attribute (transfer of thms to the
    96 current context is now done automatically);
    97 
    98 * Provers: splitter support (via 'split' attribute and 'simp' method
    99 modifier); 'simp' method: 'only:' modifier removes loopers as well
   100 (including splits);
   101 
   102 * HOL: new proof method 'cases' and improved version of 'induct' now
   103 support named cases; major packages (inductive, datatype, primrec,
   104 recdef) support case names and properly name parameters;
   105 
   106 * HOL: removed 'case_split' thm binding, should use 'cases' proof
   107 method anyway;
   108 
   109 * names of theorems etc. may be natural numbers as well;
   110 
   111 * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
   112 
   113 * 'pr' command: optional goals_limit argument; no longer prints theory
   114 contexts, but only proof states;
   115 
   116 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
   117 additional print modes to be specified; e.g. "pr(latex)" will print
   118 proof state according to the Isabelle LaTeX style;
   119 
   120 * improved support for emulating tactic scripts, including proof
   121 methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
   122 'induct_tac' (for HOL datatypes);
   123 
   124 * simplified (more robust) goal selection of proof methods: 1st goal,
   125 all goals, or explicit goal specifier (tactic emulation); thus 'proof
   126 method scripts' have to be in depth-first order;
   127 
   128 * tuned 'let' syntax: replace 'as' keyword by 'and';
   129 
   130 * theory command 'hide' removes declarations from class/type/const
   131 name spaces;
   132 
   133 
   134 *** HOL ***
   135 
   136 * HOL/Algebra: new theory of rings and univariate polynomials, by
   137 Clemens Ballarin;
   138 
   139 * HOL/record: fixed select-update simplification procedure to handle
   140 extended records as well; admit "r" as field name;
   141 
   142 * HOL/ex: new theory Factorization proving the Fundamental Theorem of
   143 Arithmetic, by Thomas M Rasmussen;
   144 
   145 * HOL/ex/Multiquote: multiple nested quotations and anti-quotations --
   146 basically a generalized version of de-Bruijn representation; very
   147 useful in avoiding lifting all operations;
   148 
   149 * HOL/Real: "rabs" replaced by overloaded "abs" function;
   150 
   151 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
   152 other numeric types and also as the identity of groups, rings, etc.;
   153 
   154 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
   155 Types nat and int belong to this axclass;
   156 
   157 * greatly improved simplification involving numerals of type nat & int, e.g.
   158    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
   159    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
   160   two terms #m*u and #n*u are replaced by #(m+n)*u
   161     (where #m, #n and u can implicitly be 1; this is simproc combine_numerals)
   162   and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
   163     or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
   164 
   165 * HOL: new version of "case_tac" subsumes both boolean case split and
   166 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
   167 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
   168 
   169 * HOL: simplification no longer dives into case-expressions: only the
   170 selector expression is simplified, but not the remaining arms. To
   171 enable full simplification of case-expressions for datatype t, you
   172 need to remove t.weak_case_cong from the simpset, either permanently
   173 (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
   174 
   175 * HOL/recdef: the recursion equations generated by 'recdef' for
   176 function 'f' are now called f.simps instead of f.rules; if all
   177 termination conditions are proved automatically, these simplification
   178 rules are added to the simpset, as in primrec; rules may be named
   179 individually as well, resulting in a separate list of theorems for
   180 each equation;
   181 
   182 * HOL: new (overloaded) notation for the set of elements below/above some
   183 element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
   184 
   185 * HOL: theorems impI, allI, ballI bound as "strip";
   186 
   187 * theory Sexp now in HOL/Induct examples (used to be part of main HOL,
   188 but was unused);
   189 
   190 * fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
   191 instead of "lfp" internally; affects ML packages only);
   192 
   193 
   194 *** General ***
   195 
   196 * improved name spaces: ambiguous output is qualified; support for
   197 hiding of names;
   198 
   199 * compression of ML heaps images may now be controlled via -c option
   200 of isabelle and isatool usedir (currently only observed by Poly/ML);
   201 
   202 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
   203 timing flag supersedes proof_timing and Toplevel.trace;
   204 
   205 * ML: new combinators |>> and |>>> for incremental transformations
   206 with secondary results (e.g. certain theory extensions):
   207 
   208 
   209 
   210 New in Isabelle99 (October 1999)
   211 --------------------------------
   212 
   213 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   214 
   215 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
   216 are no longer simplified.  (This allows the simplifier to unfold recursive
   217 functional programs.)  To restore the old behaviour, declare
   218 
   219     Delcongs [if_weak_cong];
   220 
   221 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
   222 complement;
   223 
   224 * HOL: the predicate "inj" is now defined by translation to "inj_on";
   225 
   226 * HOL/datatype: mutual_induct_tac no longer exists --
   227   use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
   228 
   229 * HOL/typedef: fixed type inference for representing set; type
   230 arguments now have to occur explicitly on the rhs as type constraints;
   231 
   232 * ZF: The con_defs part of an inductive definition may no longer refer
   233 to constants declared in the same theory;
   234 
   235 * HOL, ZF: the function mk_cases, generated by the inductive
   236 definition package, has lost an argument.  To simplify its result, it
   237 uses the default simpset instead of a supplied list of theorems.
   238 
   239 * HOL/List: the constructors of type list are now Nil and Cons;
   240 
   241 * Simplifier: the type of the infix ML functions
   242         setSSolver addSSolver setSolver addSolver
   243 is now  simpset * solver -> simpset  where `solver' is a new abstract type
   244 for packaging solvers. A solver is created via
   245         mk_solver: string -> (thm list -> int -> tactic) -> solver
   246 where the string argument is only a comment.
   247 
   248 
   249 *** Proof tools ***
   250 
   251 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
   252 decision procedure for linear arithmetic. Currently it is used for
   253 types `nat', `int', and `real' in HOL (see below); it can, should and
   254 will be instantiated for other types and logics as well.
   255 
   256 * The simplifier now accepts rewrite rules with flexible heads, eg
   257      hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
   258   They are applied like any rule with a non-pattern lhs, i.e. by first-order
   259   matching.
   260 
   261 
   262 *** General ***
   263 
   264 * New Isabelle/Isar subsystem provides an alternative to traditional
   265 tactical theorem proving; together with the ProofGeneral/isar user
   266 interface it offers an interactive environment for developing human
   267 readable proof documents (Isar == Intelligible semi-automated
   268 reasoning); for further information see isatool doc isar-ref,
   269 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/
   270 
   271 * improved presentation of theories: better HTML markup (including
   272 colors), graph views in several sizes; isatool usedir now provides a
   273 proper interface for user theories (via -P option); actual document
   274 preparation based on (PDF)LaTeX is available as well (for new-style
   275 theories only); see isatool doc system for more information;
   276 
   277 * native support for Proof General, both for classic Isabelle and
   278 Isabelle/Isar;
   279 
   280 * ML function thm_deps visualizes dependencies of theorems and lemmas,
   281 using the graph browser tool;
   282 
   283 * Isabelle manuals now also available as PDF;
   284 
   285 * theory loader rewritten from scratch (may not be fully
   286 bug-compatible); old loadpath variable has been replaced by show_path,
   287 add_path, del_path, reset_path functions; new operations such as
   288 update_thy, touch_thy, remove_thy, use/update_thy_only (see also
   289 isatool doc ref);
   290 
   291 * improved isatool install: option -k creates KDE application icon,
   292 option -p DIR installs standalone binaries;
   293 
   294 * added ML_PLATFORM setting (useful for cross-platform installations);
   295 more robust handling of platform specific ML images for SML/NJ;
   296 
   297 * the settings environment is now statically scoped, i.e. it is never
   298 created again in sub-processes invoked from isabelle, isatool, or
   299 Isabelle;
   300 
   301 * path element specification '~~' refers to '$ISABELLE_HOME';
   302 
   303 * in locales, the "assumes" and "defines" parts may be omitted if
   304 empty;
   305 
   306 * new print_mode "xsymbols" for extended symbol support (e.g. genuine
   307 long arrows);
   308 
   309 * new print_mode "HTML";
   310 
   311 * new flag show_tags controls display of tags of theorems (which are
   312 basically just comments that may be attached by some tools);
   313 
   314 * Isamode 2.6 requires patch to accomodate change of Isabelle font
   315 mode and goal output format:
   316 
   317 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el
   318 244c244
   319 <       (list (isa-getenv "ISABELLE") "-msymbols" logic-name)
   320 ---
   321 >       (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)
   322 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el
   323 181c181
   324 < (defconst proofstate-proofstart-regexp "^Level [0-9]+$"
   325 ---
   326 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"
   327 
   328 * function bind_thms stores lists of theorems (cf. bind_thm);
   329 
   330 * new shorthand tactics ftac, eatac, datac, fatac;
   331 
   332 * qed (and friends) now accept "" as result name; in that case the
   333 theorem is not stored, but proper checks and presentation of the
   334 result still apply;
   335 
   336 * theorem database now also indexes constants "Trueprop", "all",
   337 "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
   338 
   339 
   340 *** HOL ***
   341 
   342 ** HOL arithmetic **
   343 
   344 * There are now decision procedures for linear arithmetic over nat and
   345 int:
   346 
   347 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
   348 `+', `-', `Suc', `min', `max' and numerical constants; other subterms
   349 are treated as atomic; subformulae not involving type `nat' or `int'
   350 are ignored; quantified subformulae are ignored unless they are
   351 positive universal or negative existential. The tactic has to be
   352 invoked by hand and can be a little bit slow. In particular, the
   353 running time is exponential in the number of occurrences of `min' and
   354 `max', and `-' on `nat'.
   355 
   356 2. fast_arith_tac is a cut-down version of arith_tac: it only takes
   357 (negated) (in)equalities among the premises and the conclusion into
   358 account (i.e. no compound formulae) and does not know about `min' and
   359 `max', and `-' on `nat'. It is fast and is used automatically by the
   360 simplifier.
   361 
   362 NB: At the moment, these decision procedures do not cope with mixed
   363 nat/int formulae where the two parts interact, such as `m < n ==>
   364 int(m) < int(n)'.
   365 
   366 * HOL/Numeral provides a generic theory of numerals (encoded
   367 efficiently as bit strings); setup for types nat/int/real is in place;
   368 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
   369 int, existing theories and proof scripts may require a few additional
   370 type constraints;
   371 
   372 * integer division and remainder can now be performed on constant
   373 arguments;
   374 
   375 * many properties of integer multiplication, division and remainder
   376 are now available;
   377 
   378 * An interface to the Stanford Validity Checker (SVC) is available through the
   379 tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic
   380 are proved automatically.  SVC must be installed separately, and its results
   381 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any
   382 invocation of the underlying oracle).  For SVC see
   383   http://verify.stanford.edu/SVC
   384 
   385 * IsaMakefile: the HOL-Real target now builds an actual image;
   386 
   387 
   388 ** HOL misc **
   389 
   390 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
   391 (in Isabelle/Isar) -- by Gertrud Bauer;
   392 
   393 * HOL/BCV: generic model of bytecode verification, i.e. data-flow
   394 analysis for assembly languages with subtypes;
   395 
   396 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
   397 -- avoids syntactic ambiguities and treats state, transition, and
   398 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
   399 changed syntax and (many) tactics;
   400 
   401 * HOL/inductive: Now also handles more general introduction rules such
   402   as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
   403   theorems are now maintained within the theory (maintained via the
   404   "mono" attribute);
   405 
   406 * HOL/datatype: Now also handles arbitrarily branching datatypes
   407   (using function types) such as
   408 
   409   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
   410 
   411 * HOL/record: record_simproc (part of the default simpset) takes care
   412 of selectors applied to updated records; record_split_tac is no longer
   413 part of the default claset; update_defs may now be removed from the
   414 simpset in many cases; COMPATIBILITY: old behavior achieved by
   415 
   416   claset_ref () := claset() addSWrapper record_split_wrapper;
   417   Delsimprocs [record_simproc]
   418 
   419 * HOL/typedef: fixed type inference for representing set; type
   420 arguments now have to occur explicitly on the rhs as type constraints;
   421 
   422 * HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem
   423 names rather than an ML expression;
   424 
   425 * HOL/defer_recdef (TFL): like recdef but the well-founded relation can be
   426 supplied later.  Program schemes can be defined, such as
   427     "While B C s = (if B s then While B C (C s) else s)"
   428 where the well-founded relation can be chosen after B and C have been given.
   429 
   430 * HOL/List: the constructors of type list are now Nil and Cons;
   431 INCOMPATIBILITY: while [] and infix # syntax is still there, of
   432 course, ML tools referring to List.list.op # etc. have to be adapted;
   433 
   434 * HOL_quantifiers flag superseded by "HOL" print mode, which is
   435 disabled by default; run isabelle with option -m HOL to get back to
   436 the original Gordon/HOL-style output;
   437 
   438 * HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
   439 ALL x<=y. P, EX x<y. P, EX x<=y. P;
   440 
   441 * HOL basic syntax simplified (more orthogonal): all variants of
   442 All/Ex now support plain / symbolic / HOL notation; plain syntax for
   443 Eps operator is provided as well: "SOME x. P[x]";
   444 
   445 * HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
   446 
   447 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
   448 thus available for user theories;
   449 
   450 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with
   451 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
   452 time;
   453 
   454 * HOL: new tactic smp_tac: int -> int -> tactic, which applies spec
   455 several times and then mp;
   456 
   457 
   458 *** LK ***
   459 
   460 * the notation <<...>> is now available as a notation for sequences of
   461 formulas;
   462 
   463 * the simplifier is now installed
   464 
   465 * the axiom system has been generalized (thanks to Soren Heilmann)
   466 
   467 * the classical reasoner now has a default rule database
   468 
   469 
   470 *** ZF ***
   471 
   472 * new primrec section allows primitive recursive functions to be given
   473 directly (as in HOL) over datatypes and the natural numbers;
   474 
   475 * new tactics induct_tac and exhaust_tac for induction (or case
   476 analysis) over datatypes and the natural numbers;
   477 
   478 * the datatype declaration of type T now defines the recursor T_rec;
   479 
   480 * simplification automatically does freeness reasoning for datatype
   481 constructors;
   482 
   483 * automatic type-inference, with AddTCs command to insert new
   484 type-checking rules;
   485 
   486 * datatype introduction rules are now added as Safe Introduction rules
   487 to the claset;
   488 
   489 * the syntax "if P then x else y" is now available in addition to
   490 if(P,x,y);
   491 
   492 
   493 *** Internal programming interfaces ***
   494 
   495 * tuned simplifier trace output; new flag debug_simp;
   496 
   497 * structures Vartab / Termtab (instances of TableFun) offer efficient
   498 tables indexed by indexname_ord / term_ord (compatible with aconv);
   499 
   500 * AxClass.axclass_tac lost the theory argument;
   501 
   502 * tuned current_goals_markers semantics: begin / end goal avoids
   503 printing empty lines;
   504 
   505 * removed prs and prs_fn hook, which was broken because it did not
   506 include \n in its semantics, forcing writeln to add one
   507 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
   508 string -> unit if you really want to output text without newline;
   509 
   510 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
   511 plain output, interface builders may have to enable 'isabelle_font'
   512 mode to get Isabelle font glyphs as before;
   513 
   514 * refined token_translation interface; INCOMPATIBILITY: output length
   515 now of type real instead of int;
   516 
   517 * theory loader actions may be traced via new ThyInfo.add_hook
   518 interface (see src/Pure/Thy/thy_info.ML); example application: keep
   519 your own database of information attached to *whole* theories -- as
   520 opposed to intra-theory data slots offered via TheoryDataFun;
   521 
   522 * proper handling of dangling sort hypotheses (at last!);
   523 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
   524 extra sort hypotheses that can be witnessed from the type signature;
   525 the force_strip_shyps flag is gone, any remaining shyps are simply
   526 left in the theorem (with a warning issued by strip_shyps_warning);
   527 
   528 
   529 
   530 New in Isabelle98-1 (October 1998)
   531 ----------------------------------
   532 
   533 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   534 
   535 * several changes of automated proof tools;
   536 
   537 * HOL: major changes to the inductive and datatype packages, including
   538 some minor incompatibilities of theory syntax;
   539 
   540 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
   541 called `inj_on';
   542 
   543 * HOL: removed duplicate thms in Arith:
   544   less_imp_add_less  should be replaced by  trans_less_add1
   545   le_imp_add_le      should be replaced by  trans_le_add1
   546 
   547 * HOL: unary minus is now overloaded (new type constraints may be
   548 required);
   549 
   550 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
   551 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
   552 now taken as an integer constant.
   553 
   554 * Pure: ML function 'theory_of' renamed to 'theory';
   555 
   556 
   557 *** Proof tools ***
   558 
   559 * Simplifier:
   560   1. Asm_full_simp_tac is now more aggressive.
   561      1. It will sometimes reorient premises if that increases their power to
   562         simplify.
   563      2. It does no longer proceed strictly from left to right but may also
   564         rotate premises to achieve further simplification.
   565      For compatibility reasons there is now Asm_lr_simp_tac which is like the
   566      old Asm_full_simp_tac in that it does not rotate premises.
   567   2. The simplifier now knows a little bit about nat-arithmetic.
   568 
   569 * Classical reasoner: wrapper mechanism for the classical reasoner now
   570 allows for selected deletion of wrappers, by introduction of names for
   571 wrapper functionals.  This implies that addbefore, addSbefore,
   572 addaltern, and addSaltern now take a pair (name, tactic) as argument,
   573 and that adding two tactics with the same name overwrites the first
   574 one (emitting a warning).
   575   type wrapper = (int -> tactic) -> (int -> tactic)
   576   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
   577   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
   578   delWrapper, delSWrapper: claset *  string            -> claset
   579   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
   580 
   581 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
   582 semantics; addbefore now affects only the unsafe part of step_tac
   583 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
   584 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
   585 by Force_tac;
   586 
   587 * Classical reasoner: setwrapper to setWrapper and compwrapper to
   588 compWrapper; added safe wrapper (and access functions for it);
   589 
   590 * HOL/split_all_tac is now much faster and fails if there is nothing
   591 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
   592 and the names of the automatically generated variables have changed.
   593 split_all_tac has moved within claset() from unsafe wrappers to safe
   594 wrappers, which means that !!-bound variables are split much more
   595 aggressively, and safe_tac and clarify_tac now split such variables.
   596 If this splitting is not appropriate, use delSWrapper "split_all_tac".
   597 Note: the same holds for record_split_tac, which does the job of
   598 split_all_tac for record fields.
   599 
   600 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
   601 permanently to the default simpset using Addsplits just like
   602 Addsimps. They can be removed via Delsplits just like
   603 Delsimps. Lower-case versions are also available.
   604 
   605 * HOL/Simplifier: The rule split_if is now part of the default
   606 simpset. This means that the simplifier will eliminate all occurrences
   607 of if-then-else in the conclusion of a goal. To prevent this, you can
   608 either remove split_if completely from the default simpset by
   609 `Delsplits [split_if]' or remove it in a specific call of the
   610 simplifier using `... delsplits [split_if]'.  You can also add/delete
   611 other case splitting rules to/from the default simpset: every datatype
   612 generates suitable rules `split_t_case' and `split_t_case_asm' (where
   613 t is the name of the datatype).
   614 
   615 * Classical reasoner / Simplifier combination: new force_tac (and
   616 derivatives Force_tac, force) combines rewriting and classical
   617 reasoning (and whatever other tools) similarly to auto_tac, but is
   618 aimed to solve the given subgoal completely.
   619 
   620 
   621 *** General ***
   622 
   623 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
   624 and `goalw': the theory is no longer needed as an explicit argument -
   625 the current theory context is used; assumptions are no longer returned
   626 at the ML-level unless one of them starts with ==> or !!; it is
   627 recommended to convert to these new commands using isatool fixgoal
   628 (backup your sources first!);
   629 
   630 * new top-level commands 'thm' and 'thms' for retrieving theorems from
   631 the current theory context, and 'theory' to lookup stored theories;
   632 
   633 * new theory section 'locale' for declaring constants, assumptions and
   634 definitions that have local scope;
   635 
   636 * new theory section 'nonterminals' for purely syntactic types;
   637 
   638 * new theory section 'setup' for generic ML setup functions
   639 (e.g. package initialization);
   640 
   641 * the distribution now includes Isabelle icons: see
   642 lib/logo/isabelle-{small,tiny}.xpm;
   643 
   644 * isatool install - install binaries with absolute references to
   645 ISABELLE_HOME/bin;
   646 
   647 * isatool logo -- create instances of the Isabelle logo (as EPS);
   648 
   649 * print mode 'emacs' reserved for Isamode;
   650 
   651 * support multiple print (ast) translations per constant name;
   652 
   653 * theorems involving oracles are now printed with a suffixed [!];
   654 
   655 
   656 *** HOL ***
   657 
   658 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
   659 
   660 * HOL/inductive package reorganized and improved: now supports mutual
   661 definitions such as
   662 
   663   inductive EVEN ODD
   664     intrs
   665       null "0 : EVEN"
   666       oddI "n : EVEN ==> Suc n : ODD"
   667       evenI "n : ODD ==> Suc n : EVEN"
   668 
   669 new theorem list "elims" contains an elimination rule for each of the
   670 recursive sets; inductive definitions now handle disjunctive premises
   671 correctly (also ZF);
   672 
   673 INCOMPATIBILITIES: requires Inductive as an ancestor; component
   674 "mutual_induct" no longer exists - the induction rule is always
   675 contained in "induct";
   676 
   677 
   678 * HOL/datatype package re-implemented and greatly improved: now
   679 supports mutually recursive datatypes such as
   680 
   681   datatype
   682     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
   683             | SUM ('a aexp) ('a aexp)
   684             | DIFF ('a aexp) ('a aexp)
   685             | NUM 'a
   686   and
   687     'a bexp = LESS ('a aexp) ('a aexp)
   688             | AND ('a bexp) ('a bexp)
   689             | OR ('a bexp) ('a bexp)
   690 
   691 as well as indirectly recursive datatypes such as
   692 
   693   datatype
   694     ('a, 'b) term = Var 'a
   695                   | App 'b ((('a, 'b) term) list)
   696 
   697 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
   698 induction on mutually / indirectly recursive datatypes.
   699 
   700 Primrec equations are now stored in theory and can be accessed via
   701 <function_name>.simps.
   702 
   703 INCOMPATIBILITIES:
   704 
   705   - Theories using datatypes must now have theory Datatype as an
   706     ancestor.
   707   - The specific <typename>.induct_tac no longer exists - use the
   708     generic induct_tac instead.
   709   - natE has been renamed to nat.exhaust - use exhaust_tac
   710     instead of res_inst_tac ... natE. Note that the variable
   711     names in nat.exhaust differ from the names in natE, this
   712     may cause some "fragile" proofs to fail.
   713   - The theorems split_<typename>_case and split_<typename>_case_asm
   714     have been renamed to <typename>.split and <typename>.split_asm.
   715   - Since default sorts of type variables are now handled correctly,
   716     some datatype definitions may have to be annotated with explicit
   717     sort constraints.
   718   - Primrec definitions no longer require function name and type
   719     of recursive argument.
   720 
   721 Consider using isatool fixdatatype to adapt your theories and proof
   722 scripts to the new package (backup your sources first!).
   723 
   724 
   725 * HOL/record package: considerably improved implementation; now
   726 includes concrete syntax for record types, terms, updates; theorems
   727 for surjective pairing and splitting !!-bound record variables; proof
   728 support is as follows:
   729 
   730   1) standard conversions (selectors or updates applied to record
   731 constructor terms) are part of the standard simpset;
   732 
   733   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
   734 made part of standard simpset and claset via addIffs;
   735 
   736   3) a tactic for record field splitting (record_split_tac) is part of
   737 the standard claset (addSWrapper);
   738 
   739 To get a better idea about these rules you may retrieve them via
   740 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
   741 the name of your record type.
   742 
   743 The split tactic 3) conceptually simplifies by the following rule:
   744 
   745   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
   746 
   747 Thus any record variable that is bound by meta-all will automatically
   748 blow up into some record constructor term, consequently the
   749 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
   750 solve record problems automatically.
   751 
   752 
   753 * reorganized the main HOL image: HOL/Integ and String loaded by
   754 default; theory Main includes everything;
   755 
   756 * automatic simplification of integer sums and comparisons, using cancellation;
   757 
   758 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
   759 
   760 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   761 
   762 * many new identities for unions, intersections, set difference, etc.;
   763 
   764 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
   765 called split_if, split_split, split_sum_case and split_nat_case (to go
   766 with add/delsplits);
   767 
   768 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
   769 (?x::unit) = (); this is made part of the default simpset, which COULD
   770 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
   771 'Delsimprocs [unit_eq_proc];' as last resort); also note that
   772 unit_abs_eta_conv is added in order to counter the effect of
   773 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
   774 %u.f();
   775 
   776 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
   777 makes more sense);
   778 
   779 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   780   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   781   disjointness reasoning but breaking a few old proofs.
   782 
   783 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
   784 to 'converse' from 'inverse' (for compatibility with ZF and some
   785 literature);
   786 
   787 * HOL/recdef can now declare non-recursive functions, with {} supplied as
   788 the well-founded relation;
   789 
   790 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
   791     Compl A.  The "Compl" syntax remains available as input syntax for this
   792     release ONLY.
   793 
   794 * HOL/Update: new theory of function updates:
   795     f(a:=b) == %x. if x=a then b else f x
   796 may also be iterated as in f(a:=b,c:=d,...);
   797 
   798 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
   799 
   800 * HOL/List:
   801   - new function list_update written xs[i:=v] that updates the i-th
   802     list position. May also be iterated as in xs[i:=a,j:=b,...].
   803   - new function `upt' written [i..j(] which generates the list
   804     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
   805     bound write [i..j], which is a shorthand for [i..j+1(].
   806   - new lexicographic orderings and corresponding wellfoundedness theorems.
   807 
   808 * HOL/Arith:
   809   - removed 'pred' (predecessor) function;
   810   - generalized some theorems about n-1;
   811   - many new laws about "div" and "mod";
   812   - new laws about greatest common divisors (see theory ex/Primes);
   813 
   814 * HOL/Relation: renamed the relational operator r^-1 "converse"
   815 instead of "inverse";
   816 
   817 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
   818   of the multiset ordering;
   819 
   820 * directory HOL/Real: a construction of the reals using Dedekind cuts
   821   (not included by default);
   822 
   823 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   824 
   825 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
   826   programs, i.e. different program variables may have different types.
   827 
   828 * calling (stac rew i) now fails if "rew" has no effect on the goal
   829   [previously, this check worked only if the rewrite rule was unconditional]
   830   Now rew can involve either definitions or equalities (either == or =).
   831 
   832 
   833 *** ZF ***
   834 
   835 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
   836   only the theorems proved on ZF.ML;
   837 
   838 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   839   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   840   disjointness reasoning but breaking a few old proofs.
   841 
   842 * ZF/Update: new theory of function updates
   843     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
   844   may also be iterated as in f(a:=b,c:=d,...);
   845 
   846 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
   847 
   848 * calling (stac rew i) now fails if "rew" has no effect on the goal
   849   [previously, this check worked only if the rewrite rule was unconditional]
   850   Now rew can involve either definitions or equalities (either == or =).
   851 
   852 * case_tac provided for compatibility with HOL
   853     (like the old excluded_middle_tac, but with subgoals swapped)
   854 
   855 
   856 *** Internal programming interfaces ***
   857 
   858 * Pure: several new basic modules made available for general use, see
   859 also src/Pure/README;
   860 
   861 * improved the theory data mechanism to support encapsulation (data
   862 kind name replaced by private Object.kind, acting as authorization
   863 key); new type-safe user interface via functor TheoryDataFun; generic
   864 print_data function becomes basically useless;
   865 
   866 * removed global_names compatibility flag -- all theory declarations
   867 are qualified by default;
   868 
   869 * module Pure/Syntax now offers quote / antiquote translation
   870 functions (useful for Hoare logic etc. with implicit dependencies);
   871 see HOL/ex/Antiquote for an example use;
   872 
   873 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
   874 cterm -> thm;
   875 
   876 * new tactical CHANGED_GOAL for checking that a tactic modifies a
   877 subgoal;
   878 
   879 * Display.print_goals function moved to Locale.print_goals;
   880 
   881 * standard print function for goals supports current_goals_markers
   882 variable for marking begin of proof, end of proof, start of goal; the
   883 default is ("", "", ""); setting current_goals_markers := ("<proof>",
   884 "</proof>", "<goal>") causes SGML like tagged proof state printing,
   885 for example;
   886 
   887 
   888 
   889 New in Isabelle98 (January 1998)
   890 --------------------------------
   891 
   892 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   893 
   894 * changed lexical syntax of terms / types: dots made part of long
   895 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
   896 
   897 * simpset (and claset) reference variable replaced by functions
   898 simpset / simpset_ref;
   899 
   900 * no longer supports theory aliases (via merge) and non-trivial
   901 implicit merge of thms' signatures;
   902 
   903 * most internal names of constants changed due to qualified names;
   904 
   905 * changed Pure/Sequence interface (see Pure/seq.ML);
   906 
   907 
   908 *** General Changes ***
   909 
   910 * hierachically structured name spaces (for consts, types, axms, thms
   911 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
   912 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
   913 isatool fixdots ensures space after dots (e.g. "%x. x"); set
   914 long_names for fully qualified output names; NOTE: ML programs
   915 (special tactics, packages etc.) referring to internal names may have
   916 to be adapted to cope with fully qualified names; in case of severe
   917 backward campatibility problems try setting 'global_names' at compile
   918 time to have enrything declared within a flat name space; one may also
   919 fine tune name declarations in theories via the 'global' and 'local'
   920 section;
   921 
   922 * reimplemented the implicit simpset and claset using the new anytype
   923 data filed in signatures; references simpset:simpset ref etc. are
   924 replaced by functions simpset:unit->simpset and
   925 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
   926 to patch your ML files accordingly;
   927 
   928 * HTML output now includes theory graph data for display with Java
   929 applet or isatool browser; data generated automatically via isatool
   930 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
   931 
   932 * defs may now be conditional; improved rewrite_goals_tac to handle
   933 conditional equations;
   934 
   935 * defs now admits additional type arguments, using TYPE('a) syntax;
   936 
   937 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
   938 creates a new theory node; implicit merge of thms' signatures is
   939 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
   940 transfer:theory->thm->thm in (rare) cases;
   941 
   942 * improved handling of draft signatures / theories; draft thms (and
   943 ctyps, cterms) are automatically promoted to real ones;
   944 
   945 * slightly changed interfaces for oracles: admit many per theory, named
   946 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
   947 
   948 * print_goals: optional output of const types (set show_consts and
   949 show_types);
   950 
   951 * improved output of warnings (###) and errors (***);
   952 
   953 * subgoal_tac displays a warning if the new subgoal has type variables;
   954 
   955 * removed old README and Makefiles;
   956 
   957 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
   958 
   959 * removed obsolete init_pps and init_database;
   960 
   961 * deleted the obsolete tactical STATE, which was declared by
   962     fun STATE tacfun st = tacfun st st;
   963 
   964 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
   965 (which abbreviates $HOME);
   966 
   967 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
   968 use isatool fixseq to adapt your ML programs (this works for fully
   969 qualified references to the Sequence structure only!);
   970 
   971 * use_thy no longer requires writable current directory; it always
   972 reloads .ML *and* .thy file, if either one is out of date;
   973 
   974 
   975 *** Classical Reasoner ***
   976 
   977 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
   978 tactics that use classical reasoning to simplify a subgoal without
   979 splitting it into several subgoals;
   980 
   981 * Safe_tac: like safe_tac but uses the default claset;
   982 
   983 
   984 *** Simplifier ***
   985 
   986 * added simplification meta rules:
   987     (asm_)(full_)simplify: simpset -> thm -> thm;
   988 
   989 * simplifier.ML no longer part of Pure -- has to be loaded by object
   990 logics (again);
   991 
   992 * added prems argument to simplification procedures;
   993 
   994 * HOL, FOL, ZF: added infix function `addsplits':
   995   instead of `<simpset> setloop (split_tac <thms>)'
   996   you can simply write `<simpset> addsplits <thms>'
   997 
   998 
   999 *** Syntax ***
  1000 
  1001 * TYPE('a) syntax for type reflection terms;
  1002 
  1003 * no longer handles consts with name "" -- declare as 'syntax' instead;
  1004 
  1005 * pretty printer: changed order of mixfix annotation preference (again!);
  1006 
  1007 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
  1008 
  1009 
  1010 *** HOL ***
  1011 
  1012 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
  1013   with `addloop' of the simplifier to faciliate case splitting in premises.
  1014 
  1015 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
  1016 
  1017 * HOL/Auth: new protocol proofs including some for the Internet
  1018   protocol TLS;
  1019 
  1020 * HOL/Map: new theory of `maps' a la VDM;
  1021 
  1022 * HOL/simplifier: simplification procedures nat_cancel_sums for
  1023 cancelling out common nat summands from =, <, <= (in)equalities, or
  1024 differences; simplification procedures nat_cancel_factor for
  1025 cancelling common factor from =, <, <= (in)equalities over natural
  1026 sums; nat_cancel contains both kinds of procedures, it is installed by
  1027 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
  1028 
  1029 * HOL/simplifier: terms of the form
  1030   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
  1031   are rewritten to
  1032   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
  1033   and those of the form
  1034   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
  1035   are rewritten to
  1036   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
  1037 
  1038 * HOL/datatype
  1039   Each datatype `t' now comes with a theorem `split_t_case' of the form
  1040 
  1041   P(t_case f1 ... fn x) =
  1042      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
  1043         ...
  1044        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
  1045      )
  1046 
  1047   and a theorem `split_t_case_asm' of the form
  1048 
  1049   P(t_case f1 ... fn x) =
  1050     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
  1051         ...
  1052        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
  1053      )
  1054   which can be added to a simpset via `addsplits'. The existing theorems
  1055   expand_list_case and expand_option_case have been renamed to
  1056   split_list_case and split_option_case.
  1057 
  1058 * HOL/Arithmetic:
  1059   - `pred n' is automatically converted to `n-1'.
  1060     Users are strongly encouraged not to use `pred' any longer,
  1061     because it will disappear altogether at some point.
  1062   - Users are strongly encouraged to write "0 < n" rather than
  1063     "n ~= 0". Theorems and proof tools have been modified towards this
  1064     `standard'.
  1065 
  1066 * HOL/Lists:
  1067   the function "set_of_list" has been renamed "set" (and its theorems too);
  1068   the function "nth" now takes its arguments in the reverse order and
  1069   has acquired the infix notation "!" as in "xs!n".
  1070 
  1071 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
  1072 
  1073 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
  1074   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
  1075 
  1076 * HOL/record: extensible records with schematic structural subtyping
  1077 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
  1078 still lacks various theorems and concrete record syntax;
  1079 
  1080 
  1081 *** HOLCF ***
  1082 
  1083 * removed "axioms" and "generated by" sections;
  1084 
  1085 * replaced "ops" section by extended "consts" section, which is capable of
  1086   handling the continuous function space "->" directly;
  1087 
  1088 * domain package:
  1089   . proves theorems immediately and stores them in the theory,
  1090   . creates hierachical name space,
  1091   . now uses normal mixfix annotations (instead of cinfix...),
  1092   . minor changes to some names and values (for consistency),
  1093   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
  1094   . separator between mutual domain defs: changed "," to "and",
  1095   . improved handling of sort constraints;  now they have to
  1096     appear on the left-hand side of the equations only;
  1097 
  1098 * fixed LAM <x,y,zs>.b syntax;
  1099 
  1100 * added extended adm_tac to simplifier in HOLCF -- can now discharge
  1101 adm (%x. P (t x)), where P is chainfinite and t continuous;
  1102 
  1103 
  1104 *** FOL and ZF ***
  1105 
  1106 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
  1107   with `addloop' of the simplifier to faciliate case splitting in premises.
  1108 
  1109 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
  1110 in HOL, they strip ALL and --> from proved theorems;
  1111 
  1112 
  1113 
  1114 New in Isabelle94-8 (May 1997)
  1115 ------------------------------
  1116 
  1117 *** General Changes ***
  1118 
  1119 * new utilities to build / run / maintain Isabelle etc. (in parts
  1120 still somewhat experimental); old Makefiles etc. still functional;
  1121 
  1122 * new 'Isabelle System Manual';
  1123 
  1124 * INSTALL text, together with ./configure and ./build scripts;
  1125 
  1126 * reimplemented type inference for greater efficiency, better error
  1127 messages and clean internal interface;
  1128 
  1129 * prlim command for dealing with lots of subgoals (an easier way of
  1130 setting goals_limit);
  1131 
  1132 
  1133 *** Syntax ***
  1134 
  1135 * supports alternative (named) syntax tables (parser and pretty
  1136 printer); internal interface is provided by add_modesyntax(_i);
  1137 
  1138 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
  1139 be used in conjunction with the Isabelle symbol font; uses the
  1140 "symbols" syntax table;
  1141 
  1142 * added token_translation interface (may translate name tokens in
  1143 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
  1144 the current print_mode); IMPORTANT: user print translation functions
  1145 are responsible for marking newly introduced bounds
  1146 (Syntax.mark_boundT);
  1147 
  1148 * token translations for modes "xterm" and "xterm_color" that display
  1149 names in bold, underline etc. or colors (which requires a color
  1150 version of xterm);
  1151 
  1152 * infixes may now be declared with names independent of their syntax;
  1153 
  1154 * added typed_print_translation (like print_translation, but may
  1155 access type of constant);
  1156 
  1157 
  1158 *** Classical Reasoner ***
  1159 
  1160 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
  1161 some limitations.  Blast_tac...
  1162   + ignores addss, addbefore, addafter; this restriction is intrinsic
  1163   + ignores elimination rules that don't have the correct format
  1164         (the conclusion MUST be a formula variable)
  1165   + ignores types, which can make HOL proofs fail
  1166   + rules must not require higher-order unification, e.g. apply_type in ZF
  1167     [message "Function Var's argument not a bound variable" relates to this]
  1168   + its proof strategy is more general but can actually be slower
  1169 
  1170 * substitution with equality assumptions no longer permutes other
  1171 assumptions;
  1172 
  1173 * minor changes in semantics of addafter (now called addaltern); renamed
  1174 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
  1175 (and access functions for it);
  1176 
  1177 * improved combination of classical reasoner and simplifier:
  1178   + functions for handling clasimpsets
  1179   + improvement of addss: now the simplifier is called _after_ the
  1180     safe steps.
  1181   + safe variant of addss called addSss: uses safe simplifications
  1182     _during_ the safe steps. It is more complete as it allows multiple
  1183     instantiations of unknowns (e.g. with slow_tac).
  1184 
  1185 *** Simplifier ***
  1186 
  1187 * added interface for simplification procedures (functions that
  1188 produce *proven* rewrite rules on the fly, depending on current
  1189 redex);
  1190 
  1191 * ordering on terms as parameter (used for ordered rewriting);
  1192 
  1193 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
  1194 
  1195 * the solver is now split into a safe and an unsafe part.
  1196 This should be invisible for the normal user, except that the
  1197 functions setsolver and addsolver have been renamed to setSolver and
  1198 addSolver; added safe_asm_full_simp_tac;
  1199 
  1200 
  1201 *** HOL ***
  1202 
  1203 * a generic induction tactic `induct_tac' which works for all datatypes and
  1204 also for type `nat';
  1205 
  1206 * a generic case distinction tactic `exhaust_tac' which works for all
  1207 datatypes and also for type `nat';
  1208 
  1209 * each datatype comes with a function `size';
  1210 
  1211 * patterns in case expressions allow tuple patterns as arguments to
  1212 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
  1213 
  1214 * primrec now also works with type nat;
  1215 
  1216 * recdef: a new declaration form, allows general recursive functions to be
  1217 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
  1218 
  1219 * the constant for negation has been renamed from "not" to "Not" to
  1220 harmonize with FOL, ZF, LK, etc.;
  1221 
  1222 * HOL/ex/LFilter theory of a corecursive "filter" functional for
  1223 infinite lists;
  1224 
  1225 * HOL/Modelcheck demonstrates invocation of model checker oracle;
  1226 
  1227 * HOL/ex/Ring.thy declares cring_simp, which solves equational
  1228 problems in commutative rings, using axiomatic type classes for + and *;
  1229 
  1230 * more examples in HOL/MiniML and HOL/Auth;
  1231 
  1232 * more default rewrite rules for quantifiers, union/intersection;
  1233 
  1234 * a new constant `arbitrary == @x.False';
  1235 
  1236 * HOLCF/IOA replaces old HOL/IOA;
  1237 
  1238 * HOLCF changes: derived all rules and arities
  1239   + axiomatic type classes instead of classes
  1240   + typedef instead of faking type definitions
  1241   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
  1242   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
  1243   + eliminated the types void, one, tr
  1244   + use unit lift and bool lift (with translations) instead of one and tr
  1245   + eliminated blift from Lift3.thy (use Def instead of blift)
  1246   all eliminated rules are derived as theorems --> no visible changes ;
  1247 
  1248 
  1249 *** ZF ***
  1250 
  1251 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
  1252 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
  1253 as ZF_cs addSIs [equalityI];
  1254 
  1255 
  1256 
  1257 New in Isabelle94-7 (November 96)
  1258 ---------------------------------
  1259 
  1260 * allowing negative levels (as offsets) in prlev and choplev;
  1261 
  1262 * super-linear speedup for large simplifications;
  1263 
  1264 * FOL, ZF and HOL now use miniscoping: rewriting pushes
  1265 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
  1266 FAIL); can suppress it using the command Delsimps (ex_simps @
  1267 all_simps); De Morgan laws are also now included, by default;
  1268 
  1269 * improved printing of ==>  :  ~:
  1270 
  1271 * new object-logic "Sequents" adds linear logic, while replacing LK
  1272 and Modal (thanks to Sara Kalvala);
  1273 
  1274 * HOL/Auth: correctness proofs for authentication protocols;
  1275 
  1276 * HOL: new auto_tac combines rewriting and classical reasoning (many
  1277 examples on HOL/Auth);
  1278 
  1279 * HOL: new command AddIffs for declaring theorems of the form P=Q to
  1280 the rewriter and classical reasoner simultaneously;
  1281 
  1282 * function uresult no longer returns theorems in "standard" format;
  1283 regain previous version by: val uresult = standard o uresult;
  1284 
  1285 
  1286 
  1287 New in Isabelle94-6
  1288 -------------------
  1289 
  1290 * oracles -- these establish an interface between Isabelle and trusted
  1291 external reasoners, which may deliver results as theorems;
  1292 
  1293 * proof objects (in particular record all uses of oracles);
  1294 
  1295 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
  1296 
  1297 * "constdefs" section in theory files;
  1298 
  1299 * "primrec" section (HOL) no longer requires names;
  1300 
  1301 * internal type "tactic" now simply "thm -> thm Sequence.seq";
  1302 
  1303 
  1304 
  1305 New in Isabelle94-5
  1306 -------------------
  1307 
  1308 * reduced space requirements;
  1309 
  1310 * automatic HTML generation from theories;
  1311 
  1312 * theory files no longer require "..." (quotes) around most types;
  1313 
  1314 * new examples, including two proofs of the Church-Rosser theorem;
  1315 
  1316 * non-curried (1994) version of HOL is no longer distributed;
  1317 
  1318 
  1319 
  1320 New in Isabelle94-4
  1321 -------------------
  1322 
  1323 * greatly reduced space requirements;
  1324 
  1325 * theory files (.thy) no longer require \...\ escapes at line breaks;
  1326 
  1327 * searchable theorem database (see the section "Retrieving theorems" on
  1328 page 8 of the Reference Manual);
  1329 
  1330 * new examples, including Grabczewski's monumental case study of the
  1331 Axiom of Choice;
  1332 
  1333 * The previous version of HOL renamed to Old_HOL;
  1334 
  1335 * The new version of HOL (previously called CHOL) uses a curried syntax
  1336 for functions.  Application looks like f a b instead of f(a,b);
  1337 
  1338 * Mutually recursive inductive definitions finally work in HOL;
  1339 
  1340 * In ZF, pattern-matching on tuples is now available in all abstractions and
  1341 translates to the operator "split";
  1342 
  1343 
  1344 
  1345 New in Isabelle94-3
  1346 -------------------
  1347 
  1348 * new infix operator, addss, allowing the classical reasoner to
  1349 perform simplification at each step of its search.  Example:
  1350         fast_tac (cs addss ss)
  1351 
  1352 * a new logic, CHOL, the same as HOL, but with a curried syntax
  1353 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
  1354 look like (a,b) instead of <a,b>;
  1355 
  1356 * PLEASE NOTE: CHOL will eventually replace HOL!
  1357 
  1358 * In CHOL, pattern-matching on tuples is now available in all abstractions.
  1359 It translates to the operator "split".  A new theory of integers is available;
  1360 
  1361 * In ZF, integer numerals now denote two's-complement binary integers.
  1362 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
  1363 
  1364 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
  1365 of the Axiom of Choice;
  1366 
  1367 
  1368 
  1369 New in Isabelle94-2
  1370 -------------------
  1371 
  1372 * Significantly faster resolution;
  1373 
  1374 * the different sections in a .thy file can now be mixed and repeated
  1375 freely;
  1376 
  1377 * Database of theorems for FOL, HOL and ZF.  New
  1378 commands including qed, qed_goal and bind_thm store theorems in the database.
  1379 
  1380 * Simple database queries: return a named theorem (get_thm) or all theorems of
  1381 a given theory (thms_of), or find out what theory a theorem was proved in
  1382 (theory_of_thm);
  1383 
  1384 * Bugs fixed in the inductive definition and datatype packages;
  1385 
  1386 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
  1387 and HOL_dup_cs obsolete;
  1388 
  1389 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
  1390 have been removed;
  1391 
  1392 * Simpler definition of function space in ZF;
  1393 
  1394 * new results about cardinal and ordinal arithmetic in ZF;
  1395 
  1396 * 'subtype' facility in HOL for introducing new types as subsets of existing
  1397 types;
  1398 
  1399 
  1400 $Id$