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