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