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