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