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