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