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