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