NEWS
 author wenzelm Wed Oct 20 11:05:06 1999 +0200 (1999-10-20) changeset 7886 8fa551e22e52 parent 7863 8b0aca9bdc26 child 7919 35c18affc1d8 permissions -rw-r--r--
the settings environment is now statically scoped;
tuned;
```     1 Isabelle NEWS -- history user-relevant changes
```
```     2 ==============================================
```
```     3
```
```     4 New in this Isabelle version
```
```     5 ----------------------------
```
```     6
```
```     7 *** Overview of INCOMPATIBILITIES (see below for more details) ***
```
```     8
```
```     9 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
```
```    10 are no longer simplified.  (This allows the simplifier to unfold recursive
```
```    11 functional programs.)  To restore the old behaviour, declare
```
```    12
```
```    13     Delcongs [if_weak_cong];
```
```    14
```
```    15 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
```
```    16 complement;
```
```    17
```
```    18 * HOL: the predicate "inj" is now defined by translation to "inj_on";
```
```    19
```
```    20 * HOL/datatype: mutual_induct_tac no longer exists --
```
```    21   use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
```
```    22
```
```    23 * HOL/typedef: fixed type inference for representing set; type
```
```    24 arguments now have to occur explicitly on the rhs as type constraints;
```
```    25
```
```    26 * ZF: The con_defs part of an inductive definition may no longer refer
```
```    27 to constants declared in the same theory;
```
```    28
```
```    29 * HOL, ZF: the function mk_cases, generated by the inductive
```
```    30 definition package, has lost an argument.  To simplify its result, it
```
```    31 uses the default simpset instead of a supplied list of theorems.
```
```    32
```
```    33 * HOL/List: the constructors of type list are now Nil and Cons;
```
```    34
```
```    35 * Simplifier: the type of the infix ML functions
```
```    36 	setSSolver addSSolver setSolver addSolver
```
```    37 is now  simpset * solver -> simpset  where `solver' is a new abstract type
```
```    38 for packaging solvers. A solver is created via
```
```    39 	mk_solver: string -> (thm list -> int -> tactic) -> solver
```
```    40 where the string argument is only a comment.
```
```    41
```
```    42
```
```    43 *** Proof tools ***
```
```    44
```
```    45 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
```
```    46 decision procedure for linear arithmetic. Currently it is used for
```
```    47 types `nat', `int', and `real' in HOL (see below); it can, should and
```
```    48 will be instantiated for other types and logics as well.
```
```    49
```
```    50 * The simplifier now accepts rewrite rules with flexible heads, eg
```
```    51      hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
```
```    52   They are applied like any rule with a non-pattern lhs, i.e. by first-order
```
```    53   matching.
```
```    54
```
```    55
```
```    56 *** General ***
```
```    57
```
```    58 * new Isabelle/Isar subsystem provides an alternative to traditional
```
```    59 tactical theorem proving; together with the ProofGeneral/isar user
```
```    60 interface it offers an interactive environment for developing human
```
```    61 readable proof documents (Isar == Intelligible semi-automated
```
```    62 reasoning); for further information see isatool doc isar-ref,
```
```    63 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/;
```
```    64
```
```    65 * improved presentation of theories: better HTML markup (including
```
```    66 colors), graph views in several sizes; isatool usedir now provides a
```
```    67 proper interface for user theories (via -P option); actual document
```
```    68 preparation based on (PDF)LaTeX is available as well (for new-style
```
```    69 theories only); see isatool doc system for more information;
```
```    70
```
```    71 * native support for Proof General, both for classic Isabelle and
```
```    72 Isabelle/Isar (the latter is slightly better supported and more
```
```    73 robust);
```
```    74
```
```    75 * ML function thm_deps visualizes dependencies of theorems and lemmas,
```
```    76 using the graph browser tool;
```
```    77
```
```    78 * Isabelle manuals now also available as PDF;
```
```    79
```
```    80 * theory loader rewritten from scratch (may not be fully
```
```    81 bug-compatible); old loadpath variable has been replaced by show_path,
```
```    82 add_path, del_path, reset_path functions; new operations such as
```
```    83 update_thy, touch_thy, remove_thy, use/update_thy_only (see also
```
```    84 isatool doc ref);
```
```    85
```
```    86 * improved isatool install: option -k creates KDE application icon,
```
```    87 option -p DIR installs standalone binaries;
```
```    88
```
```    89 * added ML_PLATFORM setting (useful for cross-platform installations);
```
```    90 more robust handling of platform specific ML images for SML/NJ;
```
```    91
```
```    92 * the settings environment is now statically scoped, i.e. it is never
```
```    93 read again in sub-processes invoked from isabelle, isatool, or
```
```    94 Isabelle;
```
```    95
```
```    96 * path element specification '~~' refers to '\$ISABELLE_HOME';
```
```    97
```
```    98 * in locales, the "assumes" and "defines" parts may be omitted if
```
```    99 empty;
```
```   100
```
```   101 * new print_mode "xsymbols" for extended symbol support (e.g. genuine
```
```   102 long arrows);
```
```   103
```
```   104 * new print_mode "HTML";
```
```   105
```
```   106 * new flag show_tags controls display of tags of theorems (which are
```
```   107 basically just comments that may be attached by some tools);
```
```   108
```
```   109 * Isamode 2.6 requires patch to accomodate change of Isabelle font
```
```   110 mode and goal output format:
```
```   111
```
```   112 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el
```
```   113 244c244
```
```   114 <       (list (isa-getenv "ISABELLE") "-msymbols" logic-name)
```
```   115 ---
```
```   116 >       (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)
```
```   117 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el
```
```   118 181c181
```
```   119 < (defconst proofstate-proofstart-regexp "^Level [0-9]+\$"
```
```   120 ---
```
```   121 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"
```
```   122
```
```   123 * function bind_thms stores lists of theorems (cf. bind_thm);
```
```   124
```
```   125 * new shorthand tactics ftac, eatac, datac, fatac;
```
```   126
```
```   127 * qed (and friends) now accept "" as result name; in that case the
```
```   128 result is not stored, but proper checks and presentation of the result
```
```   129 still apply;
```
```   130
```
```   131 * theorem database now also indexes constants "Trueprop", "all",
```
```   132 "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
```
```   133
```
```   134
```
```   135 *** HOL ***
```
```   136
```
```   137 ** HOL arithmetic **
```
```   138
```
```   139 * There are now decision procedures for linear arithmetic over nat and
```
```   140 int:
```
```   141
```
```   142 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
```
```   143 `+', `-', `Suc', `min', `max' and numerical constants; other subterms
```
```   144 are treated as atomic; subformulae not involving type `nat' or `int'
```
```   145 are ignored; quantified subformulae are ignored unless they are
```
```   146 positive universal or negative existential. The tactic has to be
```
```   147 invoked by hand and can be a little bit slow. In particular, the
```
```   148 running time is exponential in the number of occurrences of `min' and
```
```   149 `max', and `-' on `nat'.
```
```   150
```
```   151 2. fast_arith_tac is a cut-down version of arith_tac: it only takes
```
```   152 (negated) (in)equalities among the premises and the conclusion into
```
```   153 account (i.e. no compound formulae) and does not know about `min' and
```
```   154 `max', and `-' on `nat'. It is fast and is used automatically by the
```
```   155 simplifier.
```
```   156
```
```   157 NB: At the moment, these decision procedures do not cope with mixed
```
```   158 nat/int formulae where the two parts interact, such as `m < n ==>
```
```   159 int(m) < int(n)'.
```
```   160
```
```   161 * HOL/Numeral provides a generic theory of numerals (encoded
```
```   162 efficiently as bit strings); setup for types nat/int/real is in place;
```
```   163 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
```
```   164 int, existing theories and proof scripts may require a few additional
```
```   165 type constraints;
```
```   166
```
```   167 * integer division and remainder can now be performed on constant
```
```   168 arguments;
```
```   169
```
```   170 * many properties of integer multiplication, division and remainder
```
```   171 are now available;
```
```   172
```
```   173 * An interface to the Stanford Validity Checker (SVC) is available through the
```
```   174 tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic
```
```   175 are proved automatically.  SVC must be installed separately, and its results
```
```   176 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any
```
```   177 invocation of the underlying oracle).  For SVC see
```
```   178   http://verify.stanford.edu/SVC
```
```   179
```
```   180 * IsaMakefile: the HOL-Real target now builds an actual image;
```
```   181
```
```   182
```
```   183 ** HOL misc **
```
```   184
```
```   185 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
```
```   186 (in Isabelle/Isar) -- by Gertrud Bauer;
```
```   187
```
```   188 * HOL/BCV: generic model of bytecode verification, i.e. data-flow
```
```   189 analysis for assembly languages with subtypes;
```
```   190
```
```   191 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
```
```   192 -- avoids syntactic ambiguities and treats state, transition, and
```
```   193 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
```
```   194 changed syntax and (many) tactics;
```
```   195
```
```   196 * HOL/inductive: Now also handles more general introduction rules such
```
```   197   as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
```
```   198   theorems are now maintained within the theory (maintained via the
```
```   199   "mono" attribute);
```
```   200
```
```   201 * HOL/datatype: Now also handles arbitrarily branching datatypes
```
```   202   (using function types) such as
```
```   203
```
```   204   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
```
```   205
```
```   206 * HOL/record: record_simproc (part of the default simpset) takes care
```
```   207 of selectors applied to updated records; record_split_tac is no longer
```
```   208 part of the default claset; update_defs may now be removed from the
```
```   209 simpset in many cases; COMPATIBILITY: old behavior achieved by
```
```   210
```
```   211   claset_ref () := claset() addSWrapper record_split_wrapper;
```
```   212   Delsimprocs [record_simproc]
```
```   213
```
```   214 * HOL/typedef: fixed type inference for representing set; type
```
```   215 arguments now have to occur explicitly on the rhs as type constraints;
```
```   216
```
```   217 * HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem
```
```   218 names rather than an ML expression;
```
```   219
```
```   220 * HOL/defer_recdef (TFL): like recdef but the well-founded relation can be
```
```   221 supplied later.  Program schemes can be defined, such as
```
```   222     "While B C s = (if B s then While B C (C s) else s)"
```
```   223 where the well-founded relation can be chosen after B and C have been given.
```
```   224
```
```   225 * HOL/List: the constructors of type list are now Nil and Cons;
```
```   226 INCOMPATIBILITY: while [] and infix # syntax is still there, of
```
```   227 course, ML tools referring to List.list.op # etc. have to be adapted;
```
```   228
```
```   229 * HOL_quantifiers flag superseded by "HOL" print mode, which is
```
```   230 disabled by default; run isabelle with option -m HOL to get back to
```
```   231 the original Gordon/HOL-style output;
```
```   232
```
```   233 * HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
```
```   234 ALL x<=y. P, EX x<y. P, EX x<=y. P;
```
```   235
```
```   236 * HOL basic syntax simplified (more orthogonal): all variants of
```
```   237 All/Ex now support plain / symbolic / HOL notation; plain syntax for
```
```   238 Eps operator is provided as well: "SOME x. P[x]";
```
```   239
```
```   240 * HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
```
```   241
```
```   242 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
```
```   243 thus available for user theories;
```
```   244
```
```   245 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with
```
```   246 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
```
```   247 time;
```
```   248
```
```   249 * HOL: new tactic smp_tac: int -> int -> tactic, which applies spec several
```
```   250   times and then mp
```
```   251
```
```   252
```
```   253 *** LK ***
```
```   254
```
```   255 * the notation <<...>> is now available as a notation for sequences of
```
```   256 formulas;
```
```   257
```
```   258 * the simplifier is now installed
```
```   259
```
```   260 * the axiom system has been generalized (thanks to Soren Heilmann)
```
```   261
```
```   262 * the classical reasoner now has a default rule database
```
```   263
```
```   264
```
```   265 *** ZF ***
```
```   266
```
```   267 * new primrec section allows primitive recursive functions to be given
```
```   268 directly (as in HOL) over datatypes and the natural numbers;
```
```   269
```
```   270 * new tactics induct_tac and exhaust_tac for induction (or case
```
```   271 analysis) over datatypes and the natural numbers;
```
```   272
```
```   273 * the datatype declaration of type T now defines the recursor T_rec;
```
```   274
```
```   275 * simplification automatically does freeness reasoning for datatype
```
```   276 constructors;
```
```   277
```
```   278 * automatic type-inference, with AddTCs command to insert new
```
```   279 type-checking rules;
```
```   280
```
```   281 * datatype introduction rules are now added as Safe Introduction rules
```
```   282 to the claset;
```
```   283
```
```   284 * the syntax "if P then x else y" is now available in addition to
```
```   285 if(P,x,y);
```
```   286
```
```   287
```
```   288 *** Internal programming interfaces ***
```
```   289
```
```   290 * structures Vartab / Termtab (instances of TableFun) offer efficient
```
```   291 tables indexed by indexname_ord / term_ord (compatible with aconv);
```
```   292
```
```   293 * AxClass.axclass_tac lost the theory argument;
```
```   294
```
```   295 * tuned current_goals_markers semantics: begin / end goal avoids
```
```   296 printing empty lines;
```
```   297
```
```   298 * removed prs and prs_fn hook, which was broken because it did not
```
```   299 include \n in its semantics, forcing writeln to add one
```
```   300 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
```
```   301 string -> unit if you really want to output text without newline;
```
```   302
```
```   303 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
```
```   304 plain output, interface builders may have to enable 'isabelle_font'
```
```   305 mode to get Isabelle font glyphs as before;
```
```   306
```
```   307 * refined token_translation interface; INCOMPATIBILITY: output length
```
```   308 now of type real instead of int;
```
```   309
```
```   310 * theory loader actions may be traced via new ThyInfo.add_hook
```
```   311 interface (see src/Pure/Thy/thy_info.ML); example application: keep
```
```   312 your own database of information attached to *whole* theories -- as
```
```   313 opposed to intra-theory data slots offered via TheoryDataFun;
```
```   314
```
```   315 * proper handling of dangling sort hypotheses (at last!);
```
```   316 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
```
```   317 extra sort hypotheses that can be witnessed from the type signature;
```
```   318 the force_strip_shyps is gone, any remaining shyps are simply left in
```
```   319 the theorem (with a warning issued by strip_shyps_warning);
```
```   320
```
```   321
```
```   322
```
```   323 New in Isabelle98-1 (October 1998)
```
```   324 ----------------------------------
```
```   325
```
```   326 *** Overview of INCOMPATIBILITIES (see below for more details) ***
```
```   327
```
```   328 * several changes of automated proof tools;
```
```   329
```
```   330 * HOL: major changes to the inductive and datatype packages, including
```
```   331 some minor incompatibilities of theory syntax;
```
```   332
```
```   333 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
```
```   334 called `inj_on';
```
```   335
```
```   336 * HOL: removed duplicate thms in Arith:
```
```   337   less_imp_add_less  should be replaced by  trans_less_add1
```
```   338   le_imp_add_le      should be replaced by  trans_le_add1
```
```   339
```
```   340 * HOL: unary minus is now overloaded (new type constraints may be
```
```   341 required);
```
```   342
```
```   343 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
```
```   344 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
```
```   345 now taken as an integer constant.
```
```   346
```
```   347 * Pure: ML function 'theory_of' renamed to 'theory';
```
```   348
```
```   349
```
```   350 *** Proof tools ***
```
```   351
```
```   352 * Simplifier:
```
```   353   1. Asm_full_simp_tac is now more aggressive.
```
```   354      1. It will sometimes reorient premises if that increases their power to
```
```   355         simplify.
```
```   356      2. It does no longer proceed strictly from left to right but may also
```
```   357         rotate premises to achieve further simplification.
```
```   358      For compatibility reasons there is now Asm_lr_simp_tac which is like the
```
```   359      old Asm_full_simp_tac in that it does not rotate premises.
```
```   360   2. The simplifier now knows a little bit about nat-arithmetic.
```
```   361
```
```   362 * Classical reasoner: wrapper mechanism for the classical reasoner now
```
```   363 allows for selected deletion of wrappers, by introduction of names for
```
```   364 wrapper functionals.  This implies that addbefore, addSbefore,
```
```   365 addaltern, and addSaltern now take a pair (name, tactic) as argument,
```
```   366 and that adding two tactics with the same name overwrites the first
```
```   367 one (emitting a warning).
```
```   368   type wrapper = (int -> tactic) -> (int -> tactic)
```
```   369   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
```
```   370   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
```
```   371   delWrapper, delSWrapper: claset *  string            -> claset
```
```   372   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
```
```   373
```
```   374 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
```
```   375 semantics; addbefore now affects only the unsafe part of step_tac
```
```   376 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
```
```   377 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
```
```   378 by Force_tac;
```
```   379
```
```   380 * Classical reasoner: setwrapper to setWrapper and compwrapper to
```
```   381 compWrapper; added safe wrapper (and access functions for it);
```
```   382
```
```   383 * HOL/split_all_tac is now much faster and fails if there is nothing
```
```   384 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
```
```   385 and the names of the automatically generated variables have changed.
```
```   386 split_all_tac has moved within claset() from unsafe wrappers to safe
```
```   387 wrappers, which means that !!-bound variables are split much more
```
```   388 aggressively, and safe_tac and clarify_tac now split such variables.
```
```   389 If this splitting is not appropriate, use delSWrapper "split_all_tac".
```
```   390 Note: the same holds for record_split_tac, which does the job of
```
```   391 split_all_tac for record fields.
```
```   392
```
```   393 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
```
```   394 permanently to the default simpset using Addsplits just like
```
```   395 Addsimps. They can be removed via Delsplits just like
```
```   396 Delsimps. Lower-case versions are also available.
```
```   397
```
```   398 * HOL/Simplifier: The rule split_if is now part of the default
```
```   399 simpset. This means that the simplifier will eliminate all occurrences
```
```   400 of if-then-else in the conclusion of a goal. To prevent this, you can
```
```   401 either remove split_if completely from the default simpset by
```
```   402 `Delsplits [split_if]' or remove it in a specific call of the
```
```   403 simplifier using `... delsplits [split_if]'.  You can also add/delete
```
```   404 other case splitting rules to/from the default simpset: every datatype
```
```   405 generates suitable rules `split_t_case' and `split_t_case_asm' (where
```
```   406 t is the name of the datatype).
```
```   407
```
```   408 * Classical reasoner / Simplifier combination: new force_tac (and
```
```   409 derivatives Force_tac, force) combines rewriting and classical
```
```   410 reasoning (and whatever other tools) similarly to auto_tac, but is
```
```   411 aimed to solve the given subgoal completely.
```
```   412
```
```   413
```
```   414 *** General ***
```
```   415
```
```   416 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
```
```   417 and `goalw': the theory is no longer needed as an explicit argument -
```
```   418 the current theory context is used; assumptions are no longer returned
```
```   419 at the ML-level unless one of them starts with ==> or !!; it is
```
```   420 recommended to convert to these new commands using isatool fixgoal
```
```   421 (backup your sources first!);
```
```   422
```
```   423 * new top-level commands 'thm' and 'thms' for retrieving theorems from
```
```   424 the current theory context, and 'theory' to lookup stored theories;
```
```   425
```
```   426 * new theory section 'locale' for declaring constants, assumptions and
```
```   427 definitions that have local scope;
```
```   428
```
```   429 * new theory section 'nonterminals' for purely syntactic types;
```
```   430
```
```   431 * new theory section 'setup' for generic ML setup functions
```
```   432 (e.g. package initialization);
```
```   433
```
```   434 * the distribution now includes Isabelle icons: see
```
```   435 lib/logo/isabelle-{small,tiny}.xpm;
```
```   436
```
```   437 * isatool install - install binaries with absolute references to
```
```   438 ISABELLE_HOME/bin;
```
```   439
```
```   440 * isatool logo -- create instances of the Isabelle logo (as EPS);
```
```   441
```
```   442 * print mode 'emacs' reserved for Isamode;
```
```   443
```
```   444 * support multiple print (ast) translations per constant name;
```
```   445
```
```   446 * theorems involving oracles are now printed with a suffixed [!];
```
```   447
```
```   448
```
```   449 *** HOL ***
```
```   450
```
```   451 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
```
```   452
```
```   453 * HOL/inductive package reorganized and improved: now supports mutual
```
```   454 definitions such as
```
```   455
```
```   456   inductive EVEN ODD
```
```   457     intrs
```
```   458       null "0 : EVEN"
```
```   459       oddI "n : EVEN ==> Suc n : ODD"
```
```   460       evenI "n : ODD ==> Suc n : EVEN"
```
```   461
```
```   462 new theorem list "elims" contains an elimination rule for each of the
```
```   463 recursive sets; inductive definitions now handle disjunctive premises
```
```   464 correctly (also ZF);
```
```   465
```
```   466 INCOMPATIBILITIES: requires Inductive as an ancestor; component
```
```   467 "mutual_induct" no longer exists - the induction rule is always
```
```   468 contained in "induct";
```
```   469
```
```   470
```
```   471 * HOL/datatype package re-implemented and greatly improved: now
```
```   472 supports mutually recursive datatypes such as
```
```   473
```
```   474   datatype
```
```   475     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
```
```   476             | SUM ('a aexp) ('a aexp)
```
```   477             | DIFF ('a aexp) ('a aexp)
```
```   478             | NUM 'a
```
```   479   and
```
```   480     'a bexp = LESS ('a aexp) ('a aexp)
```
```   481             | AND ('a bexp) ('a bexp)
```
```   482             | OR ('a bexp) ('a bexp)
```
```   483
```
```   484 as well as indirectly recursive datatypes such as
```
```   485
```
```   486   datatype
```
```   487     ('a, 'b) term = Var 'a
```
```   488                   | App 'b ((('a, 'b) term) list)
```
```   489
```
```   490 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
```
```   491 induction on mutually / indirectly recursive datatypes.
```
```   492
```
```   493 Primrec equations are now stored in theory and can be accessed via
```
```   494 <function_name>.simps.
```
```   495
```
```   496 INCOMPATIBILITIES:
```
```   497
```
```   498   - Theories using datatypes must now have theory Datatype as an
```
```   499     ancestor.
```
```   500   - The specific <typename>.induct_tac no longer exists - use the
```
```   501     generic induct_tac instead.
```
```   502   - natE has been renamed to nat.exhaust - use exhaust_tac
```
```   503     instead of res_inst_tac ... natE. Note that the variable
```
```   504     names in nat.exhaust differ from the names in natE, this
```
```   505     may cause some "fragile" proofs to fail.
```
```   506   - The theorems split_<typename>_case and split_<typename>_case_asm
```
```   507     have been renamed to <typename>.split and <typename>.split_asm.
```
```   508   - Since default sorts of type variables are now handled correctly,
```
```   509     some datatype definitions may have to be annotated with explicit
```
```   510     sort constraints.
```
```   511   - Primrec definitions no longer require function name and type
```
```   512     of recursive argument.
```
```   513
```
```   514 Consider using isatool fixdatatype to adapt your theories and proof
```
```   515 scripts to the new package (backup your sources first!).
```
```   516
```
```   517
```
```   518 * HOL/record package: considerably improved implementation; now
```
```   519 includes concrete syntax for record types, terms, updates; theorems
```
```   520 for surjective pairing and splitting !!-bound record variables; proof
```
```   521 support is as follows:
```
```   522
```
```   523   1) standard conversions (selectors or updates applied to record
```
```   524 constructor terms) are part of the standard simpset;
```
```   525
```
```   526   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
```
```   527 made part of standard simpset and claset via addIffs;
```
```   528
```
```   529   3) a tactic for record field splitting (record_split_tac) is part of
```
```   530 the standard claset (addSWrapper);
```
```   531
```
```   532 To get a better idea about these rules you may retrieve them via
```
```   533 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
```
```   534 the name of your record type.
```
```   535
```
```   536 The split tactic 3) conceptually simplifies by the following rule:
```
```   537
```
```   538   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
```
```   539
```
```   540 Thus any record variable that is bound by meta-all will automatically
```
```   541 blow up into some record constructor term, consequently the
```
```   542 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
```
```   543 solve record problems automatically.
```
```   544
```
```   545
```
```   546 * reorganized the main HOL image: HOL/Integ and String loaded by
```
```   547 default; theory Main includes everything;
```
```   548
```
```   549 * automatic simplification of integer sums and comparisons, using cancellation;
```
```   550
```
```   551 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
```
```   552
```
```   553 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
```
```   554
```
```   555 * many new identities for unions, intersections, set difference, etc.;
```
```   556
```
```   557 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
```
```   558 called split_if, split_split, split_sum_case and split_nat_case (to go
```
```   559 with add/delsplits);
```
```   560
```
```   561 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
```
```   562 (?x::unit) = (); this is made part of the default simpset, which COULD
```
```   563 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
```
```   564 'Delsimprocs [unit_eq_proc];' as last resort); also note that
```
```   565 unit_abs_eta_conv is added in order to counter the effect of
```
```   566 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
```
```   567 %u.f();
```
```   568
```
```   569 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
```
```   570 makes more sense);
```
```   571
```
```   572 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
```
```   573   It and 'sym RS equals0D' are now in the default  claset, giving automatic
```
```   574   disjointness reasoning but breaking a few old proofs.
```
```   575
```
```   576 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
```
```   577 to 'converse' from 'inverse' (for compatibility with ZF and some
```
```   578 literature);
```
```   579
```
```   580 * HOL/recdef can now declare non-recursive functions, with {} supplied as
```
```   581 the well-founded relation;
```
```   582
```
```   583 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
```
```   584     Compl A.  The "Compl" syntax remains available as input syntax for this
```
```   585     release ONLY.
```
```   586
```
```   587 * HOL/Update: new theory of function updates:
```
```   588     f(a:=b) == %x. if x=a then b else f x
```
```   589 may also be iterated as in f(a:=b,c:=d,...);
```
```   590
```
```   591 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
```
```   592
```
```   593 * HOL/List:
```
```   594   - new function list_update written xs[i:=v] that updates the i-th
```
```   595     list position. May also be iterated as in xs[i:=a,j:=b,...].
```
```   596   - new function `upt' written [i..j(] which generates the list
```
```   597     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
```
```   598     bound write [i..j], which is a shorthand for [i..j+1(].
```
```   599   - new lexicographic orderings and corresponding wellfoundedness theorems.
```
```   600
```
```   601 * HOL/Arith:
```
```   602   - removed 'pred' (predecessor) function;
```
```   603   - generalized some theorems about n-1;
```
```   604   - many new laws about "div" and "mod";
```
```   605   - new laws about greatest common divisors (see theory ex/Primes);
```
```   606
```
```   607 * HOL/Relation: renamed the relational operator r^-1 "converse"
```
```   608 instead of "inverse";
```
```   609
```
```   610 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
```
```   611   of the multiset ordering;
```
```   612
```
```   613 * directory HOL/Real: a construction of the reals using Dedekind cuts
```
```   614   (not included by default);
```
```   615
```
```   616 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
```
```   617
```
```   618 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
```
```   619   programs, i.e. different program variables may have different types.
```
```   620
```
```   621 * calling (stac rew i) now fails if "rew" has no effect on the goal
```
```   622   [previously, this check worked only if the rewrite rule was unconditional]
```
```   623   Now rew can involve either definitions or equalities (either == or =).
```
```   624
```
```   625
```
```   626 *** ZF ***
```
```   627
```
```   628 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
```
```   629   only the theorems proved on ZF.ML;
```
```   630
```
```   631 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
```
```   632   It and 'sym RS equals0D' are now in the default  claset, giving automatic
```
```   633   disjointness reasoning but breaking a few old proofs.
```
```   634
```
```   635 * ZF/Update: new theory of function updates
```
```   636     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
```
```   637   may also be iterated as in f(a:=b,c:=d,...);
```
```   638
```
```   639 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
```
```   640
```
```   641 * calling (stac rew i) now fails if "rew" has no effect on the goal
```
```   642   [previously, this check worked only if the rewrite rule was unconditional]
```
```   643   Now rew can involve either definitions or equalities (either == or =).
```
```   644
```
```   645 * case_tac provided for compatibility with HOL
```
```   646     (like the old excluded_middle_tac, but with subgoals swapped)
```
```   647
```
```   648
```
```   649 *** Internal programming interfaces ***
```
```   650
```
```   651 * Pure: several new basic modules made available for general use, see
```
```   652 also src/Pure/README;
```
```   653
```
```   654 * improved the theory data mechanism to support encapsulation (data
```
```   655 kind name replaced by private Object.kind, acting as authorization
```
```   656 key); new type-safe user interface via functor TheoryDataFun; generic
```
```   657 print_data function becomes basically useless;
```
```   658
```
```   659 * removed global_names compatibility flag -- all theory declarations
```
```   660 are qualified by default;
```
```   661
```
```   662 * module Pure/Syntax now offers quote / antiquote translation
```
```   663 functions (useful for Hoare logic etc. with implicit dependencies);
```
```   664 see HOL/ex/Antiquote for an example use;
```
```   665
```
```   666 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
```
```   667 cterm -> thm;
```
```   668
```
```   669 * new tactical CHANGED_GOAL for checking that a tactic modifies a
```
```   670 subgoal;
```
```   671
```
```   672 * Display.print_goals function moved to Locale.print_goals;
```
```   673
```
```   674 * standard print function for goals supports current_goals_markers
```
```   675 variable for marking begin of proof, end of proof, start of goal; the
```
```   676 default is ("", "", ""); setting current_goals_markers := ("<proof>",
```
```   677 "</proof>", "<goal>") causes SGML like tagged proof state printing,
```
```   678 for example;
```
```   679
```
```   680
```
```   681
```
```   682 New in Isabelle98 (January 1998)
```
```   683 --------------------------------
```
```   684
```
```   685 *** Overview of INCOMPATIBILITIES (see below for more details) ***
```
```   686
```
```   687 * changed lexical syntax of terms / types: dots made part of long
```
```   688 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
```
```   689
```
```   690 * simpset (and claset) reference variable replaced by functions
```
```   691 simpset / simpset_ref;
```
```   692
```
```   693 * no longer supports theory aliases (via merge) and non-trivial
```
```   694 implicit merge of thms' signatures;
```
```   695
```
```   696 * most internal names of constants changed due to qualified names;
```
```   697
```
```   698 * changed Pure/Sequence interface (see Pure/seq.ML);
```
```   699
```
```   700
```
```   701 *** General Changes ***
```
```   702
```
```   703 * hierachically structured name spaces (for consts, types, axms, thms
```
```   704 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
```
```   705 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
```
```   706 isatool fixdots ensures space after dots (e.g. "%x. x"); set
```
```   707 long_names for fully qualified output names; NOTE: ML programs
```
```   708 (special tactics, packages etc.) referring to internal names may have
```
```   709 to be adapted to cope with fully qualified names; in case of severe
```
```   710 backward campatibility problems try setting 'global_names' at compile
```
```   711 time to have enrything declared within a flat name space; one may also
```
```   712 fine tune name declarations in theories via the 'global' and 'local'
```
```   713 section;
```
```   714
```
```   715 * reimplemented the implicit simpset and claset using the new anytype
```
```   716 data filed in signatures; references simpset:simpset ref etc. are
```
```   717 replaced by functions simpset:unit->simpset and
```
```   718 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
```
```   719 to patch your ML files accordingly;
```
```   720
```
```   721 * HTML output now includes theory graph data for display with Java
```
```   722 applet or isatool browser; data generated automatically via isatool
```
```   723 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
```
```   724
```
```   725 * defs may now be conditional; improved rewrite_goals_tac to handle
```
```   726 conditional equations;
```
```   727
```
```   728 * defs now admits additional type arguments, using TYPE('a) syntax;
```
```   729
```
```   730 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
```
```   731 creates a new theory node; implicit merge of thms' signatures is
```
```   732 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
```
```   733 transfer:theory->thm->thm in (rare) cases;
```
```   734
```
```   735 * improved handling of draft signatures / theories; draft thms (and
```
```   736 ctyps, cterms) are automatically promoted to real ones;
```
```   737
```
```   738 * slightly changed interfaces for oracles: admit many per theory, named
```
```   739 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
```
```   740
```
```   741 * print_goals: optional output of const types (set show_consts and
```
```   742 show_types);
```
```   743
```
```   744 * improved output of warnings (###) and errors (***);
```
```   745
```
```   746 * subgoal_tac displays a warning if the new subgoal has type variables;
```
```   747
```
```   748 * removed old README and Makefiles;
```
```   749
```
```   750 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
```
```   751
```
```   752 * removed obsolete init_pps and init_database;
```
```   753
```
```   754 * deleted the obsolete tactical STATE, which was declared by
```
```   755     fun STATE tacfun st = tacfun st st;
```
```   756
```
```   757 * cd and use now support path variables, e.g. \$ISABELLE_HOME, or ~
```
```   758 (which abbreviates \$HOME);
```
```   759
```
```   760 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
```
```   761 use isatool fixseq to adapt your ML programs (this works for fully
```
```   762 qualified references to the Sequence structure only!);
```
```   763
```
```   764 * use_thy no longer requires writable current directory; it always
```
```   765 reloads .ML *and* .thy file, if either one is out of date;
```
```   766
```
```   767
```
```   768 *** Classical Reasoner ***
```
```   769
```
```   770 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
```
```   771 tactics that use classical reasoning to simplify a subgoal without
```
```   772 splitting it into several subgoals;
```
```   773
```
```   774 * Safe_tac: like safe_tac but uses the default claset;
```
```   775
```
```   776
```
```   777 *** Simplifier ***
```
```   778
```
```   779 * added simplification meta rules:
```
```   780     (asm_)(full_)simplify: simpset -> thm -> thm;
```
```   781
```
```   782 * simplifier.ML no longer part of Pure -- has to be loaded by object
```
```   783 logics (again);
```
```   784
```
```   785 * added prems argument to simplification procedures;
```
```   786
```
```   787 * HOL, FOL, ZF: added infix function `addsplits':
```
```   788   instead of `<simpset> setloop (split_tac <thms>)'
```
```   789   you can simply write `<simpset> addsplits <thms>'
```
```   790
```
```   791
```
```   792 *** Syntax ***
```
```   793
```
```   794 * TYPE('a) syntax for type reflection terms;
```
```   795
```
```   796 * no longer handles consts with name "" -- declare as 'syntax' instead;
```
```   797
```
```   798 * pretty printer: changed order of mixfix annotation preference (again!);
```
```   799
```
```   800 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
```
```   801
```
```   802
```
```   803 *** HOL ***
```
```   804
```
```   805 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
```
```   806   with `addloop' of the simplifier to faciliate case splitting in premises.
```
```   807
```
```   808 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
```
```   809
```
```   810 * HOL/Auth: new protocol proofs including some for the Internet
```
```   811   protocol TLS;
```
```   812
```
```   813 * HOL/Map: new theory of `maps' a la VDM;
```
```   814
```
```   815 * HOL/simplifier: simplification procedures nat_cancel_sums for
```
```   816 cancelling out common nat summands from =, <, <= (in)equalities, or
```
```   817 differences; simplification procedures nat_cancel_factor for
```
```   818 cancelling common factor from =, <, <= (in)equalities over natural
```
```   819 sums; nat_cancel contains both kinds of procedures, it is installed by
```
```   820 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
```
```   821
```
```   822 * HOL/simplifier: terms of the form
```
```   823   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
```
```   824   are rewritten to
```
```   825   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
```
```   826   and those of the form
```
```   827   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
```
```   828   are rewritten to
```
```   829   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
```
```   830
```
```   831 * HOL/datatype
```
```   832   Each datatype `t' now comes with a theorem `split_t_case' of the form
```
```   833
```
```   834   P(t_case f1 ... fn x) =
```
```   835      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
```
```   836         ...
```
```   837        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
```
```   838      )
```
```   839
```
```   840   and a theorem `split_t_case_asm' of the form
```
```   841
```
```   842   P(t_case f1 ... fn x) =
```
```   843     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
```
```   844         ...
```
```   845        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
```
```   846      )
```
```   847   which can be added to a simpset via `addsplits'. The existing theorems
```
```   848   expand_list_case and expand_option_case have been renamed to
```
```   849   split_list_case and split_option_case.
```
```   850
```
```   851 * HOL/Arithmetic:
```
```   852   - `pred n' is automatically converted to `n-1'.
```
```   853     Users are strongly encouraged not to use `pred' any longer,
```
```   854     because it will disappear altogether at some point.
```
```   855   - Users are strongly encouraged to write "0 < n" rather than
```
```   856     "n ~= 0". Theorems and proof tools have been modified towards this
```
```   857     `standard'.
```
```   858
```
```   859 * HOL/Lists:
```
```   860   the function "set_of_list" has been renamed "set" (and its theorems too);
```
```   861   the function "nth" now takes its arguments in the reverse order and
```
```   862   has acquired the infix notation "!" as in "xs!n".
```
```   863
```
```   864 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
```
```   865
```
```   866 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
```
```   867   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
```
```   868
```
```   869 * HOL/record: extensible records with schematic structural subtyping
```
```   870 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
```
```   871 still lacks various theorems and concrete record syntax;
```
```   872
```
```   873
```
```   874 *** HOLCF ***
```
```   875
```
```   876 * removed "axioms" and "generated by" sections;
```
```   877
```
```   878 * replaced "ops" section by extended "consts" section, which is capable of
```
```   879   handling the continuous function space "->" directly;
```
```   880
```
```   881 * domain package:
```
```   882   . proves theorems immediately and stores them in the theory,
```
```   883   . creates hierachical name space,
```
```   884   . now uses normal mixfix annotations (instead of cinfix...),
```
```   885   . minor changes to some names and values (for consistency),
```
```   886   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
```
```   887   . separator between mutual domain defs: changed "," to "and",
```
```   888   . improved handling of sort constraints;  now they have to
```
```   889     appear on the left-hand side of the equations only;
```
```   890
```
```   891 * fixed LAM <x,y,zs>.b syntax;
```
```   892
```
```   893 * added extended adm_tac to simplifier in HOLCF -- can now discharge
```
```   894 adm (%x. P (t x)), where P is chainfinite and t continuous;
```
```   895
```
```   896
```
```   897 *** FOL and ZF ***
```
```   898
```
```   899 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
```
```   900   with `addloop' of the simplifier to faciliate case splitting in premises.
```
```   901
```
```   902 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
```
```   903 in HOL, they strip ALL and --> from proved theorems;
```
```   904
```
```   905
```
```   906
```
```   907 New in Isabelle94-8 (May 1997)
```
```   908 ------------------------------
```
```   909
```
```   910 *** General Changes ***
```
```   911
```
```   912 * new utilities to build / run / maintain Isabelle etc. (in parts
```
```   913 still somewhat experimental); old Makefiles etc. still functional;
```
```   914
```
```   915 * new 'Isabelle System Manual';
```
```   916
```
```   917 * INSTALL text, together with ./configure and ./build scripts;
```
```   918
```
```   919 * reimplemented type inference for greater efficiency, better error
```
```   920 messages and clean internal interface;
```
```   921
```
```   922 * prlim command for dealing with lots of subgoals (an easier way of
```
```   923 setting goals_limit);
```
```   924
```
```   925
```
```   926 *** Syntax ***
```
```   927
```
```   928 * supports alternative (named) syntax tables (parser and pretty
```
```   929 printer); internal interface is provided by add_modesyntax(_i);
```
```   930
```
```   931 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
```
```   932 be used in conjunction with the Isabelle symbol font; uses the
```
```   933 "symbols" syntax table;
```
```   934
```
```   935 * added token_translation interface (may translate name tokens in
```
```   936 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
```
```   937 the current print_mode); IMPORTANT: user print translation functions
```
```   938 are responsible for marking newly introduced bounds
```
```   939 (Syntax.mark_boundT);
```
```   940
```
```   941 * token translations for modes "xterm" and "xterm_color" that display
```
```   942 names in bold, underline etc. or colors (which requires a color
```
```   943 version of xterm);
```
```   944
```
```   945 * infixes may now be declared with names independent of their syntax;
```
```   946
```
```   947 * added typed_print_translation (like print_translation, but may
```
```   948 access type of constant);
```
```   949
```
```   950
```
```   951 *** Classical Reasoner ***
```
```   952
```
```   953 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
```
```   954 some limitations.  Blast_tac...
```
```   955   + ignores addss, addbefore, addafter; this restriction is intrinsic
```
```   956   + ignores elimination rules that don't have the correct format
```
```   957         (the conclusion MUST be a formula variable)
```
```   958   + ignores types, which can make HOL proofs fail
```
```   959   + rules must not require higher-order unification, e.g. apply_type in ZF
```
```   960     [message "Function Var's argument not a bound variable" relates to this]
```
```   961   + its proof strategy is more general but can actually be slower
```
```   962
```
```   963 * substitution with equality assumptions no longer permutes other
```
```   964 assumptions;
```
```   965
```
```   966 * minor changes in semantics of addafter (now called addaltern); renamed
```
```   967 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
```
```   968 (and access functions for it);
```
```   969
```
```   970 * improved combination of classical reasoner and simplifier:
```
```   971   + functions for handling clasimpsets
```
```   972   + improvement of addss: now the simplifier is called _after_ the
```
```   973     safe steps.
```
```   974   + safe variant of addss called addSss: uses safe simplifications
```
```   975     _during_ the safe steps. It is more complete as it allows multiple
```
```   976     instantiations of unknowns (e.g. with slow_tac).
```
```   977
```
```   978 *** Simplifier ***
```
```   979
```
```   980 * added interface for simplification procedures (functions that
```
```   981 produce *proven* rewrite rules on the fly, depending on current
```
```   982 redex);
```
```   983
```
```   984 * ordering on terms as parameter (used for ordered rewriting);
```
```   985
```
```   986 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
```
```   987
```
```   988 * the solver is now split into a safe and an unsafe part.
```
```   989 This should be invisible for the normal user, except that the
```
```   990 functions setsolver and addsolver have been renamed to setSolver and
```
```   991 addSolver; added safe_asm_full_simp_tac;
```
```   992
```
```   993
```
```   994 *** HOL ***
```
```   995
```
```   996 * a generic induction tactic `induct_tac' which works for all datatypes and
```
```   997 also for type `nat';
```
```   998
```
```   999 * a generic case distinction tactic `exhaust_tac' which works for all
```
```  1000 datatypes and also for type `nat';
```
```  1001
```
```  1002 * each datatype comes with a function `size';
```
```  1003
```
```  1004 * patterns in case expressions allow tuple patterns as arguments to
```
```  1005 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
```
```  1006
```
```  1007 * primrec now also works with type nat;
```
```  1008
```
```  1009 * recdef: a new declaration form, allows general recursive functions to be
```
```  1010 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
```
```  1011
```
```  1012 * the constant for negation has been renamed from "not" to "Not" to
```
```  1013 harmonize with FOL, ZF, LK, etc.;
```
```  1014
```
```  1015 * HOL/ex/LFilter theory of a corecursive "filter" functional for
```
```  1016 infinite lists;
```
```  1017
```
```  1018 * HOL/Modelcheck demonstrates invocation of model checker oracle;
```
```  1019
```
```  1020 * HOL/ex/Ring.thy declares cring_simp, which solves equational
```
```  1021 problems in commutative rings, using axiomatic type classes for + and *;
```
```  1022
```
```  1023 * more examples in HOL/MiniML and HOL/Auth;
```
```  1024
```
```  1025 * more default rewrite rules for quantifiers, union/intersection;
```
```  1026
```
```  1027 * a new constant `arbitrary == @x.False';
```
```  1028
```
```  1029 * HOLCF/IOA replaces old HOL/IOA;
```
```  1030
```
```  1031 * HOLCF changes: derived all rules and arities
```
```  1032   + axiomatic type classes instead of classes
```
```  1033   + typedef instead of faking type definitions
```
```  1034   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
```
```  1035   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
```
```  1036   + eliminated the types void, one, tr
```
```  1037   + use unit lift and bool lift (with translations) instead of one and tr
```
```  1038   + eliminated blift from Lift3.thy (use Def instead of blift)
```
```  1039   all eliminated rules are derived as theorems --> no visible changes ;
```
```  1040
```
```  1041
```
```  1042 *** ZF ***
```
```  1043
```
```  1044 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
```
```  1045 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
```
```  1046 as ZF_cs addSIs [equalityI];
```
```  1047
```
```  1048
```
```  1049
```
```  1050 New in Isabelle94-7 (November 96)
```
```  1051 ---------------------------------
```
```  1052
```
```  1053 * allowing negative levels (as offsets) in prlev and choplev;
```
```  1054
```
```  1055 * super-linear speedup for large simplifications;
```
```  1056
```
```  1057 * FOL, ZF and HOL now use miniscoping: rewriting pushes
```
```  1058 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
```
```  1059 FAIL); can suppress it using the command Delsimps (ex_simps @
```
```  1060 all_simps); De Morgan laws are also now included, by default;
```
```  1061
```
```  1062 * improved printing of ==>  :  ~:
```
```  1063
```
```  1064 * new object-logic "Sequents" adds linear logic, while replacing LK
```
```  1065 and Modal (thanks to Sara Kalvala);
```
```  1066
```
```  1067 * HOL/Auth: correctness proofs for authentication protocols;
```
```  1068
```
```  1069 * HOL: new auto_tac combines rewriting and classical reasoning (many
```
```  1070 examples on HOL/Auth);
```
```  1071
```
```  1072 * HOL: new command AddIffs for declaring theorems of the form P=Q to
```
```  1073 the rewriter and classical reasoner simultaneously;
```
```  1074
```
```  1075 * function uresult no longer returns theorems in "standard" format;
```
```  1076 regain previous version by: val uresult = standard o uresult;
```
```  1077
```
```  1078
```
```  1079
```
```  1080 New in Isabelle94-6
```
```  1081 -------------------
```
```  1082
```
```  1083 * oracles -- these establish an interface between Isabelle and trusted
```
```  1084 external reasoners, which may deliver results as theorems;
```
```  1085
```
```  1086 * proof objects (in particular record all uses of oracles);
```
```  1087
```
```  1088 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
```
```  1089
```
```  1090 * "constdefs" section in theory files;
```
```  1091
```
```  1092 * "primrec" section (HOL) no longer requires names;
```
```  1093
```
```  1094 * internal type "tactic" now simply "thm -> thm Sequence.seq";
```
```  1095
```
```  1096
```
```  1097
```
```  1098 New in Isabelle94-5
```
```  1099 -------------------
```
```  1100
```
```  1101 * reduced space requirements;
```
```  1102
```
```  1103 * automatic HTML generation from theories;
```
```  1104
```
```  1105 * theory files no longer require "..." (quotes) around most types;
```
```  1106
```
```  1107 * new examples, including two proofs of the Church-Rosser theorem;
```
```  1108
```
```  1109 * non-curried (1994) version of HOL is no longer distributed;
```
```  1110
```
```  1111
```
```  1112
```
```  1113 New in Isabelle94-4
```
```  1114 -------------------
```
```  1115
```
```  1116 * greatly reduced space requirements;
```
```  1117
```
```  1118 * theory files (.thy) no longer require \...\ escapes at line breaks;
```
```  1119
```
```  1120 * searchable theorem database (see the section "Retrieving theorems" on
```
```  1121 page 8 of the Reference Manual);
```
```  1122
```
```  1123 * new examples, including Grabczewski's monumental case study of the
```
```  1124 Axiom of Choice;
```
```  1125
```
```  1126 * The previous version of HOL renamed to Old_HOL;
```
```  1127
```
```  1128 * The new version of HOL (previously called CHOL) uses a curried syntax
```
```  1129 for functions.  Application looks like f a b instead of f(a,b);
```
```  1130
```
```  1131 * Mutually recursive inductive definitions finally work in HOL;
```
```  1132
```
```  1133 * In ZF, pattern-matching on tuples is now available in all abstractions and
```
```  1134 translates to the operator "split";
```
```  1135
```
```  1136
```
```  1137
```
```  1138 New in Isabelle94-3
```
```  1139 -------------------
```
```  1140
```
```  1141 * new infix operator, addss, allowing the classical reasoner to
```
```  1142 perform simplification at each step of its search.  Example:
```
```  1143         fast_tac (cs addss ss)
```
```  1144
```
```  1145 * a new logic, CHOL, the same as HOL, but with a curried syntax
```
```  1146 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
```
```  1147 look like (a,b) instead of <a,b>;
```
```  1148
```
```  1149 * PLEASE NOTE: CHOL will eventually replace HOL!
```
```  1150
```
```  1151 * In CHOL, pattern-matching on tuples is now available in all abstractions.
```
```  1152 It translates to the operator "split".  A new theory of integers is available;
```
```  1153
```
```  1154 * In ZF, integer numerals now denote two's-complement binary integers.
```
```  1155 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
```
```  1156
```
```  1157 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
```
```  1158 of the Axiom of Choice;
```
```  1159
```
```  1160
```
```  1161
```
```  1162 New in Isabelle94-2
```
```  1163 -------------------
```
```  1164
```
```  1165 * Significantly faster resolution;
```
```  1166
```
```  1167 * the different sections in a .thy file can now be mixed and repeated
```
```  1168 freely;
```
```  1169
```
```  1170 * Database of theorems for FOL, HOL and ZF.  New
```
```  1171 commands including qed, qed_goal and bind_thm store theorems in the database.
```
```  1172
```
```  1173 * Simple database queries: return a named theorem (get_thm) or all theorems of
```
```  1174 a given theory (thms_of), or find out what theory a theorem was proved in
```
```  1175 (theory_of_thm);
```
```  1176
```
```  1177 * Bugs fixed in the inductive definition and datatype packages;
```
```  1178
```
```  1179 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
```
```  1180 and HOL_dup_cs obsolete;
```
```  1181
```
```  1182 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
```
```  1183 have been removed;
```
```  1184
```
```  1185 * Simpler definition of function space in ZF;
```
```  1186
```
```  1187 * new results about cardinal and ordinal arithmetic in ZF;
```
```  1188
```
```  1189 * 'subtype' facility in HOL for introducing new types as subsets of existing
```
```  1190 types;
```
```  1191
```
```  1192
```
```  1193 \$Id\$
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.780097,"math_prob":0.8234549,"size":43989,"snap":"2019-51-2020-05","text_gpt3_token_len":11010,"char_repetition_ratio":0.115562126,"word_repetition_ratio":0.0385875,"special_character_ratio":0.2909591,"punctuation_ratio":0.13918817,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.95346117,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-01-23T05:45:53Z\",\"WARC-Record-ID\":\"<urn:uuid:6a892e70-5c57-4c67-b9a9-717d53e4621d>\",\"Content-Length\":\"194977\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:136a9a6c-e079-444f-89e2-94d2034f93f7>\",\"WARC-Concurrent-To\":\"<urn:uuid:ffd6d855-d6b5-40ed-b922-ecd1a75f3664>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"https://isabelle.in.tum.de/repos/isabelle/file/8fa551e22e52/NEWS\",\"WARC-Payload-Digest\":\"sha1:OINHHQLCH2XXF3WUB7JRWTVGCI56QGGH\",\"WARC-Block-Digest\":\"sha1:UT3KSYI2I5FZLT5GZ3S3MC3SK4AK6VAJ\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-05/CC-MAIN-2020-05_segments_1579250608295.52_warc_CC-MAIN-20200123041345-20200123070345-00340.warc.gz\"}"}