NEWS
author wenzelm
Sat Nov 13 12:32:21 2010 +0100 (2010-11-13 ago)
changeset 40521 8896bd93488e
parent 40424 7550b2cba1cb
child 40580 0592d3a39c08
permissions -rw-r--r--
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     3 
     4 New in this Isabelle version
     5 ----------------------------
     6 
     7 *** General ***
     8 
     9 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
    10 (and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
    11 while the default heap location within that directory lacks that extra
    12 suffix.  This isolates multiple Isabelle installations from each
    13 other, avoiding problems with old settings in new versions.
    14 INCOMPATIBILITY, need to copy/upgrade old user settings manually.
    15 
    16 * Significantly improved Isabelle/Isar implementation manual.
    17 
    18 * Explicit treatment of UTF8 sequences as Isabelle symbols, such that
    19 a Unicode character is treated as a single symbol, not a sequence of
    20 non-ASCII bytes as before.  Since Isabelle/ML string literals may
    21 contain symbols without further backslash escapes, Unicode can now be
    22 used here as well.  Recall that Symbol.explode in ML provides a
    23 consistent view on symbols, while raw explode (or String.explode)
    24 merely give a byte-oriented representation.
    25 
    26 * Theory loading: only the master source file is looked-up in the
    27 implicit load path, all other files are addressed relatively to its
    28 directory.  Minor INCOMPATIBILITY, subtle change in semantics.
    29 
    30 * Special treatment of ML file names has been discontinued.
    31 Historically, optional extensions .ML or .sml were added on demand --
    32 at the cost of clarity of file dependencies.  Recall that Isabelle/ML
    33 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
    34 
    35 * Various options that affect pretty printing etc. are now properly
    36 handled within the context via configuration options, instead of
    37 unsynchronized references.  There are both ML Config.T entities and
    38 Isar declaration attributes to access these.
    39 
    40   ML (Config.T)                 Isar (attribute)
    41 
    42   eta_contract                  eta_contract
    43   show_brackets                 show_brackets
    44   show_sorts                    show_sorts
    45   show_types                    show_types
    46   show_question_marks           show_question_marks
    47   show_consts                   show_consts
    48 
    49   Syntax.ambiguity_level        syntax_ambiguity_level
    50 
    51   Goal_Display.goals_limit      goals_limit
    52   Goal_Display.show_main_goal   show_main_goal
    53 
    54   Thy_Output.display            thy_output_display
    55   Thy_Output.quotes             thy_output_quotes
    56   Thy_Output.indent             thy_output_indent
    57   Thy_Output.source             thy_output_source
    58   Thy_Output.break              thy_output_break
    59 
    60 Note that corresponding "..._default" references in ML may be only
    61 changed globally at the ROOT session setup, but *not* within a theory.
    62 
    63 
    64 *** Pure ***
    65 
    66 * Support for real valued configuration options, using simplistic
    67 floating-point notation that coincides with the inner syntax for
    68 float_token.
    69 
    70 * Support for real valued preferences (with approximative PGIP type).
    71 
    72 * Interpretation command 'interpret' accepts a list of equations like
    73 'interpretation' does.
    74 
    75 * Diagnostic command 'print_interps' prints interpretations in proofs
    76 in addition to interpretations in theories.
    77 
    78 * Discontinued obsolete 'global' and 'local' commands to manipulate
    79 the theory name space.  Rare INCOMPATIBILITY.  The ML functions
    80 Sign.root_path and Sign.local_path may be applied directly where this
    81 feature is still required for historical reasons.
    82 
    83 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
    84 'definition' instead.
    85 
    86 * Document antiquotations @{class} and @{type} for printing classes
    87 and type constructors.
    88 
    89 
    90 *** HOL ***
    91 
    92 * Theory Multiset provides stable quicksort implementation of sort_key.
    93 
    94 * Quickcheck now has a configurable time limit which is set to 30 seconds
    95 by default. This can be changed by adding [timeout = n] to the quickcheck
    96 command. The time limit for auto quickcheck is still set independently,
    97 by default to 5 seconds.
    98 
    99 * New command 'partial_function' provides basic support for recursive
   100 function definitions over complete partial orders. Concrete instances
   101 are provided for i) the option type, ii) tail recursion on arbitrary
   102 types, and iii) the heap monad of Imperative_HOL. See
   103 HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
   104 examples.
   105 
   106 * Predicates `distinct` and `sorted` now defined inductively, with nice
   107 induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
   108 now named distinct_simps and sorted_simps.
   109 
   110 * Constant `contents` renamed to `the_elem`, to free the generic name
   111 contents for other uses.  INCOMPATIBILITY.
   112 
   113 * Dropped old primrec package.  INCOMPATIBILITY.
   114 
   115 * Improved infrastructure for term evaluation using code generator
   116 techniques, in particular static evaluation conversions.
   117 
   118 * String.literal is a type, but not a datatype.  INCOMPATIBILITY.
   119  
   120 * Renamed lemmas:
   121   expand_fun_eq -> fun_eq_iff
   122   expand_set_eq -> set_eq_iff
   123   set_ext -> set_eqI
   124  INCOMPATIBILITY.
   125 
   126 * Renamed lemma list: nat_number -> eval_nat_numeral
   127 
   128 * Renamed class eq and constant eq (for code generation) to class equal
   129 and constant equal, plus renaming of related facts and various tuning.
   130 INCOMPATIBILITY.
   131 
   132 * Scala (2.8 or higher) has been added to the target languages of
   133 the code generator.
   134 
   135 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
   136 
   137 * Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
   138 
   139 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
   140 canonical names for instance definitions for functions; various improvements.
   141 INCOMPATIBILITY.
   142 
   143 * Records: logical foundation type for records do not carry a '_type' suffix
   144 any longer.  INCOMPATIBILITY.
   145 
   146 * Code generation for records: more idiomatic representation of record types.
   147 Warning: records are not covered by ancient SML code generation any longer.
   148 INCOMPATIBILITY.  In cases of need, a suitable rep_datatype declaration
   149 helps to succeed then:
   150 
   151   record 'a foo = ...
   152   ...
   153   rep_datatype foo_ext ...
   154 
   155 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.
   156 INCOMPATIBILITY.
   157 
   158 * Quickcheck in locales considers interpretations of that locale for
   159 counter example search.
   160 
   161 * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
   162 in Library/State_Monad has been changed to avoid ambiguities.
   163 INCOMPATIBILITY.
   164 
   165 * Code generator: export_code without explicit file declaration prints
   166 to standard output.  INCOMPATIBILITY.
   167 
   168 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
   169 respectively.  INCOMPATIBILITY.
   170 
   171 * Name "Plus" of disjoint sum operator "<+>" is now hidden.
   172   Write Sum_Type.Plus.
   173 
   174 * Constant "split" has been merged with constant "prod_case";  names
   175 of ML functions, facts etc. involving split have been retained so far,
   176 though.  INCOMPATIBILITY.
   177 
   178 * Dropped old infix syntax "mem" for List.member;  use "in set"
   179 instead.  INCOMPATIBILITY.
   180 
   181 * Refactoring of code-generation specific operations in List.thy
   182 
   183   constants
   184     null ~> List.null
   185 
   186   facts
   187     mem_iff ~> member_def
   188     null_empty ~> null_def
   189 
   190 INCOMPATIBILITY.  Note that these were not suppossed to be used
   191 regularly unless for striking reasons;  their main purpose was code
   192 generation.
   193 
   194 * Some previously unqualified names have been qualified:
   195 
   196   types
   197     bool ~> HOL.bool
   198     nat ~> Nat.nat
   199 
   200   constants
   201     Trueprop ~> HOL.Trueprop
   202     True ~> HOL.True
   203     False ~> HOL.False
   204     op & ~> HOL.conj
   205     op | ~> HOL.disj
   206     op --> ~> HOL.implies
   207     op = ~> HOL.eq
   208     Not ~> HOL.Not
   209     The ~> HOL.The
   210     All ~> HOL.All
   211     Ex ~> HOL.Ex
   212     Ex1 ~> HOL.Ex1
   213     Let ~> HOL.Let
   214     If ~> HOL.If
   215     Ball ~> Set.Ball
   216     Bex ~> Set.Bex
   217     Suc ~> Nat.Suc
   218     Pair ~> Product_Type.Pair
   219     fst ~> Product_Type.fst
   220     snd ~> Product_Type.snd
   221     curry ~> Product_Type.curry
   222     op : ~> Set.member
   223     Collect ~> Set.Collect
   224 
   225 INCOMPATIBILITY.
   226 
   227 * Removed simplifier congruence rule of "prod_case", as has for long
   228 been the case with "split".  INCOMPATIBILITY.
   229 
   230 * Datatype package: theorems generated for executable equality
   231 (class eq) carry proper names and are treated as default code
   232 equations.
   233 
   234 * Removed lemma Option.is_none_none (Duplicate of is_none_def).
   235 INCOMPATIBILITY.
   236 
   237 * List.thy: use various operations from the Haskell prelude when
   238 generating Haskell code.
   239 
   240 * Multiset.thy: renamed empty_idemp -> empty_neutral
   241 
   242 * code_simp.ML and method code_simp: simplification with rules determined
   243 by code generator.
   244 
   245 * code generator: do not print function definitions for case
   246 combinators any longer.
   247 
   248 * Multivariate Analysis: Introduced a type class for euclidean space. Most
   249 theorems are now stated in terms of euclidean spaces instead of finite
   250 cartesian products.
   251 
   252   types
   253     real ^ 'n ~>  'a::real_vector
   254               ~>  'a::euclidean_space
   255               ~>  'a::ordered_euclidean_space
   256         (depends on your needs)
   257 
   258   constants
   259      _ $ _        ~> _ $$ _
   260      \<chi> x. _  ~> \<chi>\<chi> x. _
   261      CARD('n)     ~> DIM('a)
   262 
   263 Also note that the indices are now natural numbers and not from some finite
   264 type. Finite cartesian products of euclidean spaces, products of euclidean
   265 spaces the real and complex numbers are instantiated to be euclidean_spaces.
   266 
   267 INCOMPATIBILITY.
   268 
   269 * Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal
   270 as value for measures. Introduces Lebesgue Measure based on the integral in
   271 Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure
   272 spaces.
   273 
   274  INCOMPATIBILITY.
   275 
   276 * Inductive package: offers new command "inductive_simps" to automatically
   277 derive instantiated and simplified equations for inductive predicates,
   278 similar to inductive_cases.
   279 
   280 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
   281 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
   282 The theorems bij_def and surj_def are unchanged.
   283 
   284 * Function package: .psimps rules are no longer implicitly declared [simp].
   285 INCOMPATIBILITY.
   286 
   287 * Weaker versions of the "meson" and "metis" proof methods are now available in
   288   "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become
   289   more powerful after "Hilbert_Choice" is loaded in "HOL-Main".
   290 
   291 * MESON: Renamed lemmas:
   292   meson_not_conjD ~> Meson.not_conjD
   293   meson_not_disjD ~> Meson.not_disjD
   294   meson_not_notD ~> Meson.not_notD
   295   meson_not_allD ~> Meson.not_allD
   296   meson_not_exD ~> Meson.not_exD
   297   meson_imp_to_disjD ~> Meson.imp_to_disjD
   298   meson_not_impD ~> Meson.not_impD
   299   meson_iff_to_disjD ~> Meson.iff_to_disjD
   300   meson_not_iffD ~> Meson.not_iffD
   301   meson_not_refl_disj_D ~> Meson.not_refl_disj_D
   302   meson_conj_exD1 ~> Meson.conj_exD1
   303   meson_conj_exD2 ~> Meson.conj_exD2
   304   meson_disj_exD ~> Meson.disj_exD
   305   meson_disj_exD1 ~> Meson.disj_exD1
   306   meson_disj_exD2 ~> Meson.disj_exD2
   307   meson_disj_assoc ~> Meson.disj_assoc
   308   meson_disj_comm ~> Meson.disj_comm
   309   meson_disj_FalseD1 ~> Meson.disj_FalseD1
   310   meson_disj_FalseD2 ~> Meson.disj_FalseD2
   311 INCOMPATIBILITY.
   312 
   313 * Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as
   314   "solve_direct".
   315 
   316 * Sledgehammer:
   317   - Renamed lemmas:
   318     COMBI_def ~> Meson.COMBI_def
   319     COMBK_def ~> Meson.COMBK_def
   320     COMBB_def ~> Meson.COMBB_def
   321     COMBC_def ~> Meson.COMBC_def
   322     COMBS_def ~> Meson.COMBS_def
   323     abs_I ~> Meson.abs_I
   324     abs_K ~> Meson.abs_K
   325     abs_B ~> Meson.abs_B
   326     abs_C ~> Meson.abs_C
   327     abs_S ~> Meson.abs_S
   328     INCOMPATIBILITY.
   329   - Renamed commands:
   330     sledgehammer atp_info ~> sledgehammer running_provers
   331     sledgehammer atp_kill ~> sledgehammer kill_provers
   332     sledgehammer available_atps ~> sledgehammer available_provers
   333     INCOMPATIBILITY.
   334   - Renamed options:
   335     sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
   336     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
   337     sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
   338     (and "ms" and "min" are no longer supported)
   339     INCOMPATIBILITY.
   340 
   341 * Nitpick:
   342   - Renamed options:
   343     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
   344     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
   345     INCOMPATIBILITY.
   346 
   347 * Changed SMT configuration options:
   348   - Renamed:
   349     z3_proofs ~> smt_oracle (with swapped semantics)
   350     z3_trace_assms ~> smt_trace_used_facts
   351     INCOMPATIBILITY.
   352   - Added:
   353     smt_verbose
   354     smt_datatypes
   355     cvc3_options
   356     yices_options
   357 
   358 * Removed [split_format ... and ... and ...] version of
   359 [split_format].  Potential INCOMPATIBILITY.
   360 
   361 *** FOL ***
   362 
   363 * All constant names are now qualified.  INCOMPATIBILITY.
   364 
   365 
   366 *** ZF ***
   367 
   368 * All constant names are now qualified.  INCOMPATIBILITY.
   369 
   370 
   371 *** ML ***
   372 
   373 * Discontinued obsolete function sys_error and exception SYS_ERROR.
   374 See implementation manual for further details on exceptions in
   375 Isabelle/ML.
   376 
   377 * Antiquotation @{assert} inlines a function bool -> unit that raises
   378 Fail if the argument is false.  Due to inlining the source position of
   379 failed assertions is included in the error output.
   380 
   381 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML
   382 text is in practice always evaluated with a stable theory checkpoint.
   383 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
   384 
   385 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
   386 meaning.
   387 
   388 * Renamed structure PureThy to Pure_Thy and moved most of its
   389 operations to structure Global_Theory, to emphasize that this is
   390 rarely-used global-only stuff.
   391 
   392 * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
   393 instead (or tracing for high-volume output).
   394 
   395 * Configuration option show_question_marks only affects regular pretty
   396 printing of types and terms, not raw Term.string_of_vname.
   397 
   398 * ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
   399 INCOMPATIBILITY, superseded by static antiquotations @{thm} and
   400 @{thms} for most purposes.
   401 
   402 * ML structure Unsynchronized never opened, not even in Isar
   403 interaction mode as before.  Old Unsynchronized.set etc. have been
   404 discontinued -- use plain := instead.  This should be *rare* anyway,
   405 since modern tools always work via official context data, notably
   406 configuration options.
   407 
   408 * ML antiquotations @{theory} and @{theory_ref} refer to named
   409 theories from the ancestry of the current context, not any accidental
   410 theory loader state as before.  Potential INCOMPATIBILITY, subtle
   411 change in semantics.
   412 
   413 * Parallel and asynchronous execution requires special care concerning
   414 interrupts.  Structure Exn provides some convenience functions that
   415 avoid working directly with raw Interrupt.  User code must not absorb
   416 interrupts -- intermediate handling (for cleanup etc.) needs to be
   417 followed by re-raising of the original exception.  Another common
   418 source of mistakes are "handle _" patterns, which make the meaning of
   419 the program subject to physical effects of the environment.
   420 
   421 
   422 *** System ***
   423 
   424 * Discontinued support for Poly/ML 5.0 and 5.1 versions.
   425 
   426 
   427 
   428 New in Isabelle2009-2 (June 2010)
   429 ---------------------------------
   430 
   431 *** General ***
   432 
   433 * Authentic syntax for *all* logical entities (type classes, type
   434 constructors, term constants): provides simple and robust
   435 correspondence between formal entities and concrete syntax.  Within
   436 the parse tree / AST representations, "constants" are decorated by
   437 their category (class, type, const) and spelled out explicitly with
   438 their full internal name.
   439 
   440 Substantial INCOMPATIBILITY concerning low-level syntax declarations
   441 and translations (translation rules and translation functions in ML).
   442 Some hints on upgrading:
   443 
   444   - Many existing uses of 'syntax' and 'translations' can be replaced
   445     by more modern 'type_notation', 'notation' and 'abbreviation',
   446     which are independent of this issue.
   447 
   448   - 'translations' require markup within the AST; the term syntax
   449     provides the following special forms:
   450 
   451       CONST c   -- produces syntax version of constant c from context
   452       XCONST c  -- literally c, checked as constant from context
   453       c         -- literally c, if declared by 'syntax'
   454 
   455     Plain identifiers are treated as AST variables -- occasionally the
   456     system indicates accidental variables via the error "rhs contains
   457     extra variables".
   458 
   459     Type classes and type constructors are marked according to their
   460     concrete syntax.  Some old translations rules need to be written
   461     for the "type" category, using type constructor application
   462     instead of pseudo-term application of the default category
   463     "logic".
   464 
   465   - 'parse_translation' etc. in ML may use the following
   466     antiquotations:
   467 
   468       @{class_syntax c}   -- type class c within parse tree / AST
   469       @{term_syntax c}    -- type constructor c within parse tree / AST
   470       @{const_syntax c}   -- ML version of "CONST c" above
   471       @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
   472 
   473   - Literal types within 'typed_print_translations', i.e. those *not*
   474     represented as pseudo-terms are represented verbatim.  Use @{class
   475     c} or @{type_name c} here instead of the above syntax
   476     antiquotations.
   477 
   478 Note that old non-authentic syntax was based on unqualified base
   479 names, so all of the above "constant" names would coincide.  Recall
   480 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
   481 diagnose syntax problems.
   482 
   483 * Type constructors admit general mixfix syntax, not just infix.
   484 
   485 * Concrete syntax may be attached to local entities without a proof
   486 body, too.  This works via regular mixfix annotations for 'fix',
   487 'def', 'obtain' etc. or via the explicit 'write' command, which is
   488 similar to the 'notation' command in theory specifications.
   489 
   490 * Discontinued unnamed infix syntax (legacy feature for many years) --
   491 need to specify constant name and syntax separately.  Internal ML
   492 datatype constructors have been renamed from InfixName to Infix etc.
   493 Minor INCOMPATIBILITY.
   494 
   495 * Schematic theorem statements need to be explicitly markup as such,
   496 via commands 'schematic_lemma', 'schematic_theorem',
   497 'schematic_corollary'.  Thus the relevance of the proof is made
   498 syntactically clear, which impacts performance in a parallel or
   499 asynchronous interactive environment.  Minor INCOMPATIBILITY.
   500 
   501 * Use of cumulative prems via "!" in some proof methods has been
   502 discontinued (old legacy feature).
   503 
   504 * References 'trace_simp' and 'debug_simp' have been replaced by
   505 configuration options stored in the context. Enabling tracing (the
   506 case of debugging is similar) in proofs works via
   507 
   508   using [[trace_simp = true]]
   509 
   510 Tracing is then active for all invocations of the simplifier in
   511 subsequent goal refinement steps. Tracing may also still be enabled or
   512 disabled via the ProofGeneral settings menu.
   513 
   514 * Separate commands 'hide_class', 'hide_type', 'hide_const',
   515 'hide_fact' replace the former 'hide' KIND command.  Minor
   516 INCOMPATIBILITY.
   517 
   518 * Improved parallelism of proof term normalization: usedir -p2 -q0 is
   519 more efficient than combinations with -q1 or -q2.
   520 
   521 
   522 *** Pure ***
   523 
   524 * Proofterms record type-class reasoning explicitly, using the
   525 "unconstrain" operation internally.  This eliminates all sort
   526 constraints from a theorem and proof, introducing explicit
   527 OFCLASS-premises.  On the proof term level, this operation is
   528 automatically applied at theorem boundaries, such that closed proofs
   529 are always free of sort constraints.  INCOMPATIBILITY for tools that
   530 inspect proof terms.
   531 
   532 * Local theory specifications may depend on extra type variables that
   533 are not present in the result type -- arguments TYPE('a) :: 'a itself
   534 are added internally.  For example:
   535 
   536   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
   537 
   538 * Predicates of locales introduced by classes carry a mandatory
   539 "class" prefix.  INCOMPATIBILITY.
   540 
   541 * Vacuous class specifications observe default sort.  INCOMPATIBILITY.
   542 
   543 * Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use
   544 'class' instead.
   545 
   546 * Command 'code_reflect' allows to incorporate generated ML code into
   547 runtime environment; replaces immature code_datatype antiquotation.
   548 INCOMPATIBILITY.
   549 
   550 * Code generator: simple concept for abstract datatypes obeying
   551 invariants.
   552 
   553 * Code generator: details of internal data cache have no impact on the
   554 user space functionality any longer.
   555 
   556 * Methods "unfold_locales" and "intro_locales" ignore non-locale
   557 subgoals.  This is more appropriate for interpretations with 'where'.
   558 INCOMPATIBILITY.
   559 
   560 * Command 'example_proof' opens an empty proof body.  This allows to
   561 experiment with Isar, without producing any persistent result.
   562 
   563 * Commands 'type_notation' and 'no_type_notation' declare type syntax
   564 within a local theory context, with explicit checking of the
   565 constructors involved (in contrast to the raw 'syntax' versions).
   566 
   567 * Commands 'types' and 'typedecl' now work within a local theory
   568 context -- without introducing dependencies on parameters or
   569 assumptions, which is not possible in Isabelle/Pure.
   570 
   571 * Command 'defaultsort' has been renamed to 'default_sort', it works
   572 within a local theory context.  Minor INCOMPATIBILITY.
   573 
   574 
   575 *** HOL ***
   576 
   577 * Command 'typedef' now works within a local theory context -- without
   578 introducing dependencies on parameters or assumptions, which is not
   579 possible in Isabelle/Pure/HOL.  Note that the logical environment may
   580 contain multiple interpretations of local typedefs (with different
   581 non-emptiness proofs), even in a global theory context.
   582 
   583 * New package for quotient types.  Commands 'quotient_type' and
   584 'quotient_definition' may be used for defining types and constants by
   585 quotient constructions.  An example is the type of integers created by
   586 quotienting pairs of natural numbers:
   587 
   588   fun
   589     intrel :: "(nat * nat) => (nat * nat) => bool"
   590   where
   591     "intrel (x, y) (u, v) = (x + v = u + y)"
   592 
   593   quotient_type int = "nat * nat" / intrel
   594     by (auto simp add: equivp_def expand_fun_eq)
   595 
   596   quotient_definition
   597     "0::int" is "(0::nat, 0::nat)"
   598 
   599 The method "lifting" can be used to lift of theorems from the
   600 underlying "raw" type to the quotient type.  The example
   601 src/HOL/Quotient_Examples/FSet.thy includes such a quotient
   602 construction and provides a reasoning infrastructure for finite sets.
   603 
   604 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
   605 clash with new theory Quotient in Main HOL.
   606 
   607 * Moved the SMT binding into the main HOL session, eliminating
   608 separate HOL-SMT session.
   609 
   610 * List membership infix mem operation is only an input abbreviation.
   611 INCOMPATIBILITY.
   612 
   613 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy
   614 for future developements; former Library/Word.thy is still present in
   615 the AFP entry RSAPPS.
   616 
   617 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
   618 longer shadowed.  INCOMPATIBILITY.
   619 
   620 * Dropped theorem duplicate comp_arith; use semiring_norm instead.
   621 INCOMPATIBILITY.
   622 
   623 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
   624 INCOMPATIBILITY.
   625 
   626 * Dropped normalizing_semiring etc; use the facts in semiring classes
   627 instead.  INCOMPATIBILITY.
   628 
   629 * Dropped several real-specific versions of lemmas about floor and
   630 ceiling; use the generic lemmas from theory "Archimedean_Field"
   631 instead.  INCOMPATIBILITY.
   632 
   633   floor_number_of_eq         ~> floor_number_of
   634   le_floor_eq_number_of      ~> number_of_le_floor
   635   le_floor_eq_zero           ~> zero_le_floor
   636   le_floor_eq_one            ~> one_le_floor
   637   floor_less_eq_number_of    ~> floor_less_number_of
   638   floor_less_eq_zero         ~> floor_less_zero
   639   floor_less_eq_one          ~> floor_less_one
   640   less_floor_eq_number_of    ~> number_of_less_floor
   641   less_floor_eq_zero         ~> zero_less_floor
   642   less_floor_eq_one          ~> one_less_floor
   643   floor_le_eq_number_of      ~> floor_le_number_of
   644   floor_le_eq_zero           ~> floor_le_zero
   645   floor_le_eq_one            ~> floor_le_one
   646   floor_subtract_number_of   ~> floor_diff_number_of
   647   floor_subtract_one         ~> floor_diff_one
   648   ceiling_number_of_eq       ~> ceiling_number_of
   649   ceiling_le_eq_number_of    ~> ceiling_le_number_of
   650   ceiling_le_zero_eq         ~> ceiling_le_zero
   651   ceiling_le_eq_one          ~> ceiling_le_one
   652   less_ceiling_eq_number_of  ~> number_of_less_ceiling
   653   less_ceiling_eq_zero       ~> zero_less_ceiling
   654   less_ceiling_eq_one        ~> one_less_ceiling
   655   ceiling_less_eq_number_of  ~> ceiling_less_number_of
   656   ceiling_less_eq_zero       ~> ceiling_less_zero
   657   ceiling_less_eq_one        ~> ceiling_less_one
   658   le_ceiling_eq_number_of    ~> number_of_le_ceiling
   659   le_ceiling_eq_zero         ~> zero_le_ceiling
   660   le_ceiling_eq_one          ~> one_le_ceiling
   661   ceiling_subtract_number_of ~> ceiling_diff_number_of
   662   ceiling_subtract_one       ~> ceiling_diff_one
   663 
   664 * Theory "Finite_Set": various folding_XXX locales facilitate the
   665 application of the various fold combinators on finite sets.
   666 
   667 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
   668 provides abstract red-black tree type which is backed by "RBT_Impl" as
   669 implementation.  INCOMPATIBILTY.
   670 
   671 * Theory Library/Coinductive_List has been removed -- superseded by
   672 AFP/thys/Coinductive.
   673 
   674 * Theory PReal, including the type "preal" and related operations, has
   675 been removed.  INCOMPATIBILITY.
   676 
   677 * Real: new development using Cauchy Sequences.
   678 
   679 * Split off theory "Big_Operators" containing setsum, setprod,
   680 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
   681 
   682 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
   683 "Int" etc.  INCOMPATIBILITY.
   684 
   685 * Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.
   686 
   687 * New set of rules "ac_simps" provides combined assoc / commute
   688 rewrites for all interpretations of the appropriate generic locales.
   689 
   690 * Renamed theory "OrderedGroup" to "Groups" and split theory
   691 "Ring_and_Field" into theories "Rings" and "Fields"; for more
   692 appropriate and more consistent names suitable for name prefixes
   693 within the HOL theories.  INCOMPATIBILITY.
   694 
   695 * Some generic constants have been put to appropriate theories:
   696   - less_eq, less: Orderings
   697   - zero, one, plus, minus, uminus, times, abs, sgn: Groups
   698   - inverse, divide: Rings
   699 INCOMPATIBILITY.
   700 
   701 * More consistent naming of type classes involving orderings (and
   702 lattices):
   703 
   704     lower_semilattice                   ~> semilattice_inf
   705     upper_semilattice                   ~> semilattice_sup
   706 
   707     dense_linear_order                  ~> dense_linorder
   708 
   709     pordered_ab_group_add               ~> ordered_ab_group_add
   710     pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
   711     pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
   712     pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
   713     pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
   714     pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
   715     pordered_cancel_semiring            ~> ordered_cancel_semiring
   716     pordered_comm_monoid_add            ~> ordered_comm_monoid_add
   717     pordered_comm_ring                  ~> ordered_comm_ring
   718     pordered_comm_semiring              ~> ordered_comm_semiring
   719     pordered_ring                       ~> ordered_ring
   720     pordered_ring_abs                   ~> ordered_ring_abs
   721     pordered_semiring                   ~> ordered_semiring
   722 
   723     ordered_ab_group_add                ~> linordered_ab_group_add
   724     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
   725     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
   726     ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
   727     ordered_field                       ~> linordered_field
   728     ordered_field_no_lb                 ~> linordered_field_no_lb
   729     ordered_field_no_ub                 ~> linordered_field_no_ub
   730     ordered_field_dense_linear_order    ~> dense_linordered_field
   731     ordered_idom                        ~> linordered_idom
   732     ordered_ring                        ~> linordered_ring
   733     ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
   734     ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
   735     ordered_ring_strict                 ~> linordered_ring_strict
   736     ordered_semidom                     ~> linordered_semidom
   737     ordered_semiring                    ~> linordered_semiring
   738     ordered_semiring_1                  ~> linordered_semiring_1
   739     ordered_semiring_1_strict           ~> linordered_semiring_1_strict
   740     ordered_semiring_strict             ~> linordered_semiring_strict
   741 
   742   The following slightly odd type classes have been moved to a
   743   separate theory Library/Lattice_Algebras:
   744 
   745     lordered_ab_group_add               ~> lattice_ab_group_add
   746     lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
   747     lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
   748     lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
   749     lordered_ring                       ~> lattice_ring
   750 
   751 INCOMPATIBILITY.
   752 
   753 * Refined field classes:
   754   - classes division_ring_inverse_zero, field_inverse_zero,
   755     linordered_field_inverse_zero include rule inverse 0 = 0 --
   756     subsumes former division_by_zero class;
   757   - numerous lemmas have been ported from field to division_ring.
   758 INCOMPATIBILITY.
   759 
   760 * Refined algebra theorem collections:
   761   - dropped theorem group group_simps, use algebra_simps instead;
   762   - dropped theorem group ring_simps, use field_simps instead;
   763   - proper theorem collection field_simps subsumes former theorem
   764     groups field_eq_simps and field_simps;
   765   - dropped lemma eq_minus_self_iff which is a duplicate for
   766     equal_neg_zero.
   767 INCOMPATIBILITY.
   768 
   769 * Theory Finite_Set and List: some lemmas have been generalized from
   770 sets to lattices:
   771 
   772   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
   773   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
   774   inter_Inter_fold_inter        ~> inf_Inf_fold_inf
   775   union_Union_fold_union        ~> sup_Sup_fold_sup
   776   Inter_fold_inter              ~> Inf_fold_inf
   777   Union_fold_union              ~> Sup_fold_sup
   778   inter_INTER_fold_inter        ~> inf_INFI_fold_inf
   779   union_UNION_fold_union        ~> sup_SUPR_fold_sup
   780   INTER_fold_inter              ~> INFI_fold_inf
   781   UNION_fold_union              ~> SUPR_fold_sup
   782 
   783 * Theory "Complete_Lattice": lemmas top_def and bot_def have been
   784 replaced by the more convenient lemmas Inf_empty and Sup_empty.
   785 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
   786 by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
   787 former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
   788 subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
   789 
   790 * Reorganized theory Multiset: swapped notation of pointwise and
   791 multiset order:
   792 
   793   - pointwise ordering is instance of class order with standard syntax
   794     <= and <;
   795   - multiset ordering has syntax <=# and <#; partial order properties
   796     are provided by means of interpretation with prefix
   797     multiset_order;
   798   - less duplication, less historical organization of sections,
   799     conversion from associations lists to multisets, rudimentary code
   800     generation;
   801   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
   802     if needed.
   803 
   804 Renamed:
   805 
   806   multiset_eq_conv_count_eq  ~>  multiset_ext_iff
   807   multi_count_ext  ~>  multiset_ext
   808   diff_union_inverse2  ~>  diff_union_cancelR
   809 
   810 INCOMPATIBILITY.
   811 
   812 * Theory Permutation: replaced local "remove" by List.remove1.
   813 
   814 * Code generation: ML and OCaml code is decorated with signatures.
   815 
   816 * Theory List: added transpose.
   817 
   818 * Library/Nat_Bijection.thy is a collection of bijective functions
   819 between nat and other types, which supersedes the older libraries
   820 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
   821 
   822   Constants:
   823   Nat_Int_Bij.nat2_to_nat         ~> prod_encode
   824   Nat_Int_Bij.nat_to_nat2         ~> prod_decode
   825   Nat_Int_Bij.int_to_nat_bij      ~> int_encode
   826   Nat_Int_Bij.nat_to_int_bij      ~> int_decode
   827   Countable.pair_encode           ~> prod_encode
   828   NatIso.prod2nat                 ~> prod_encode
   829   NatIso.nat2prod                 ~> prod_decode
   830   NatIso.sum2nat                  ~> sum_encode
   831   NatIso.nat2sum                  ~> sum_decode
   832   NatIso.list2nat                 ~> list_encode
   833   NatIso.nat2list                 ~> list_decode
   834   NatIso.set2nat                  ~> set_encode
   835   NatIso.nat2set                  ~> set_decode
   836 
   837   Lemmas:
   838   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
   839   Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
   840   Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
   841   Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
   842   Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
   843   Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
   844   Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
   845   Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
   846   Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
   847   Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
   848   Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
   849   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
   850   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
   851 
   852 * Sledgehammer:
   853   - Renamed ATP commands:
   854     atp_info     ~> sledgehammer running_atps
   855     atp_kill     ~> sledgehammer kill_atps
   856     atp_messages ~> sledgehammer messages
   857     atp_minimize ~> sledgehammer minimize
   858     print_atps   ~> sledgehammer available_atps
   859     INCOMPATIBILITY.
   860   - Added user's manual ("isabelle doc sledgehammer").
   861   - Added option syntax and "sledgehammer_params" to customize
   862     Sledgehammer's behavior.  See the manual for details.
   863   - Modified the Isar proof reconstruction code so that it produces
   864     direct proofs rather than proofs by contradiction.  (This feature
   865     is still experimental.)
   866   - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
   867     full-typed mode.
   868   - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
   869 
   870 * Nitpick:
   871   - Added and implemented "binary_ints" and "bits" options.
   872   - Added "std" option and implemented support for nonstandard models.
   873   - Added and implemented "finitize" option to improve the precision
   874     of infinite datatypes based on a monotonicity analysis.
   875   - Added support for quotient types.
   876   - Added support for "specification" and "ax_specification"
   877     constructs.
   878   - Added support for local definitions (for "function" and
   879     "termination" proofs).
   880   - Added support for term postprocessors.
   881   - Optimized "Multiset.multiset" and "FinFun.finfun".
   882   - Improved efficiency of "destroy_constrs" optimization.
   883   - Fixed soundness bugs related to "destroy_constrs" optimization and
   884     record getters.
   885   - Fixed soundness bug related to higher-order constructors.
   886   - Fixed soundness bug when "full_descrs" is enabled.
   887   - Improved precision of set constructs.
   888   - Added "atoms" option.
   889   - Added cache to speed up repeated Kodkod invocations on the same
   890     problems.
   891   - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
   892     "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
   893     "SAT4J_Light".  INCOMPATIBILITY.
   894   - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
   895     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
   896   - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
   897 
   898 * Method "induct" now takes instantiations of the form t, where t is not
   899   a variable, as a shorthand for "x == t", where x is a fresh variable.
   900   If this is not intended, t has to be enclosed in parentheses.
   901   By default, the equalities generated by definitional instantiations
   902   are pre-simplified, which may cause parameters of inductive cases
   903   to disappear, or may even delete some of the inductive cases.
   904   Use "induct (no_simp)" instead of "induct" to restore the old
   905   behaviour. The (no_simp) option is also understood by the "cases"
   906   and "nominal_induct" methods, which now perform pre-simplification, too.
   907   INCOMPATIBILITY.
   908 
   909 
   910 *** HOLCF ***
   911 
   912 * Variable names in lemmas generated by the domain package have
   913 changed; the naming scheme is now consistent with the HOL datatype
   914 package.  Some proof scripts may be affected, INCOMPATIBILITY.
   915 
   916 * The domain package no longer defines the function "foo_copy" for
   917 recursive domain "foo".  The reach lemma is now stated directly in
   918 terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
   919 be reformulated in terms of "foo_take", INCOMPATIBILITY.
   920 
   921 * Most definedness lemmas generated by the domain package (previously
   922 of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
   923 like "foo$x = UU <-> x = UU", which works better as a simp rule.
   924 Proofs that used definedness lemmas as intro rules may break,
   925 potential INCOMPATIBILITY.
   926 
   927 * Induction and casedist rules generated by the domain package now
   928 declare proper case_names (one called "bottom", and one named for each
   929 constructor).  INCOMPATIBILITY.
   930 
   931 * For mutually-recursive domains, separate "reach" and "take_lemma"
   932 rules are generated for each domain, INCOMPATIBILITY.
   933 
   934   foo_bar.reach       ~> foo.reach  bar.reach
   935   foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
   936 
   937 * Some lemmas generated by the domain package have been renamed for
   938 consistency with the datatype package, INCOMPATIBILITY.
   939 
   940   foo.ind        ~> foo.induct
   941   foo.finite_ind ~> foo.finite_induct
   942   foo.coind      ~> foo.coinduct
   943   foo.casedist   ~> foo.exhaust
   944   foo.exhaust    ~> foo.nchotomy
   945 
   946 * For consistency with other definition packages, the fixrec package
   947 now generates qualified theorem names, INCOMPATIBILITY.
   948 
   949   foo_simps  ~> foo.simps
   950   foo_unfold ~> foo.unfold
   951   foo_induct ~> foo.induct
   952 
   953 * The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
   954 method and internal fixrec proofs now use the default simpset instead.
   955 INCOMPATIBILITY.
   956 
   957 * The "contlub" predicate has been removed.  Proof scripts should use
   958 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
   959 
   960 * The "admw" predicate has been removed, INCOMPATIBILITY.
   961 
   962 * The constants cpair, cfst, and csnd have been removed in favor of
   963 Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
   964 
   965 
   966 *** ML ***
   967 
   968 * Antiquotations for basic formal entities:
   969 
   970     @{class NAME}         -- type class
   971     @{class_syntax NAME}  -- syntax representation of the above
   972 
   973     @{type_name NAME}     -- logical type
   974     @{type_abbrev NAME}   -- type abbreviation
   975     @{nonterminal NAME}   -- type of concrete syntactic category
   976     @{type_syntax NAME}   -- syntax representation of any of the above
   977 
   978     @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
   979     @{const_abbrev NAME}  -- abbreviated constant
   980     @{const_syntax NAME}  -- syntax representation of any of the above
   981 
   982 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
   983 syntax constant (cf. 'syntax' command).
   984 
   985 * Antiquotation @{make_string} inlines a function to print arbitrary
   986 values similar to the ML toplevel.  The result is compiler dependent
   987 and may fall back on "?" in certain situations.
   988 
   989 * Diagnostic commands 'ML_val' and 'ML_command' may refer to
   990 antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
   991 Isar.state() and Isar.goal(), which belong to the old TTY loop and do
   992 not work with the asynchronous Isar document model.
   993 
   994 * Configuration options now admit dynamic default values, depending on
   995 the context or even global references.
   996 
   997 * SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
   998 uses an efficient external library if available (for Poly/ML).
   999 
  1000 * Renamed some important ML structures, while keeping the old names
  1001 for some time as aliases within the structure Legacy:
  1002 
  1003   OuterKeyword  ~>  Keyword
  1004   OuterLex      ~>  Token
  1005   OuterParse    ~>  Parse
  1006   OuterSyntax   ~>  Outer_Syntax
  1007   PrintMode     ~>  Print_Mode
  1008   SpecParse     ~>  Parse_Spec
  1009   ThyInfo       ~>  Thy_Info
  1010   ThyLoad       ~>  Thy_Load
  1011   ThyOutput     ~>  Thy_Output
  1012   TypeInfer     ~>  Type_Infer
  1013 
  1014 Note that "open Legacy" simplifies porting of sources, but forgetting
  1015 to remove it again will complicate porting again in the future.
  1016 
  1017 * Most operations that refer to a global context are named
  1018 accordingly, e.g. Simplifier.global_context or
  1019 ProofContext.init_global.  There are some situations where a global
  1020 context actually works, but under normal circumstances one needs to
  1021 pass the proper local context through the code!
  1022 
  1023 * Discontinued old TheoryDataFun with its copy/init operation -- data
  1024 needs to be pure.  Functor Theory_Data_PP retains the traditional
  1025 Pretty.pp argument to merge, which is absent in the standard
  1026 Theory_Data version.
  1027 
  1028 * Sorts.certify_sort and derived "cert" operations for types and terms
  1029 no longer minimize sorts.  Thus certification at the boundary of the
  1030 inference kernel becomes invariant under addition of class relations,
  1031 which is an important monotonicity principle.  Sorts are now minimized
  1032 in the syntax layer only, at the boundary between the end-user and the
  1033 system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
  1034 explicitly in rare situations.
  1035 
  1036 * Renamed old-style Drule.standard to Drule.export_without_context, to
  1037 emphasize that this is in no way a standard operation.
  1038 INCOMPATIBILITY.
  1039 
  1040 * Subgoal.FOCUS (and variants): resulting goal state is normalized as
  1041 usual for resolution.  Rare INCOMPATIBILITY.
  1042 
  1043 * Renamed varify/unvarify operations to varify_global/unvarify_global
  1044 to emphasize that these only work in a global situation (which is
  1045 quite rare).
  1046 
  1047 * Curried take and drop in library.ML; negative length is interpreted
  1048 as infinity (as in chop).  Subtle INCOMPATIBILITY.
  1049 
  1050 * Proof terms: type substitutions on proof constants now use canonical
  1051 order of type variables.  INCOMPATIBILITY for tools working with proof
  1052 terms.
  1053 
  1054 * Raw axioms/defs may no longer carry sort constraints, and raw defs
  1055 may no longer carry premises.  User-level specifications are
  1056 transformed accordingly by Thm.add_axiom/add_def.
  1057 
  1058 
  1059 *** System ***
  1060 
  1061 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
  1062 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
  1063 proof terms are enabled unconditionally in the new HOL-Proofs image.
  1064 
  1065 * Discontinued old ISABELLE and ISATOOL environment settings (legacy
  1066 feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
  1067 respectively.
  1068 
  1069 * Old lib/scripts/polyml-platform is superseded by the
  1070 ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
  1071 variant, even on a 64 bit machine.  The following example setting
  1072 prefers 64 bit if available:
  1073 
  1074   ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
  1075 
  1076 * The preliminary Isabelle/jEdit application demonstrates the emerging
  1077 Isabelle/Scala layer for advanced prover interaction and integration.
  1078 See src/Tools/jEdit or "isabelle jedit" provided by the properly built
  1079 component.
  1080 
  1081 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
  1082 and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
  1083 similar to the default assignment of the document preparation system
  1084 (cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
  1085 provides some operations for direct access to the font without asking
  1086 the user for manual installation.
  1087 
  1088 
  1089 
  1090 New in Isabelle2009-1 (December 2009)
  1091 -------------------------------------
  1092 
  1093 *** General ***
  1094 
  1095 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only
  1096 one backslash should be used, even in ML sources.
  1097 
  1098 
  1099 *** Pure ***
  1100 
  1101 * Locale interpretation propagates mixins along the locale hierarchy.
  1102 The currently only available mixins are the equations used to map
  1103 local definitions to terms of the target domain of an interpretation.
  1104 
  1105 * Reactivated diagnostic command 'print_interps'.  Use "print_interps
  1106 loc" to print all interpretations of locale "loc" in the theory.
  1107 Interpretations in proofs are not shown.
  1108 
  1109 * Thoroughly revised locales tutorial.  New section on conditional
  1110 interpretation.
  1111 
  1112 * On instantiation of classes, remaining undefined class parameters
  1113 are formally declared.  INCOMPATIBILITY.
  1114 
  1115 
  1116 *** Document preparation ***
  1117 
  1118 * New generalized style concept for printing terms: @{foo (style) ...}
  1119 instead of @{foo_style style ...}  (old form is still retained for
  1120 backward compatibility).  Styles can be also applied for
  1121 antiquotations prop, term_type and typeof.
  1122 
  1123 
  1124 *** HOL ***
  1125 
  1126 * New proof method "smt" for a combination of first-order logic with
  1127 equality, linear and nonlinear (natural/integer/real) arithmetic, and
  1128 fixed-size bitvectors; there is also basic support for higher-order
  1129 features (esp. lambda abstractions).  It is an incomplete decision
  1130 procedure based on external SMT solvers using the oracle mechanism;
  1131 for the SMT solver Z3, this method is proof-producing.  Certificates
  1132 are provided to avoid calling the external solvers solely for
  1133 re-checking proofs.  Due to a remote SMT service there is no need for
  1134 installing SMT solvers locally.  See src/HOL/SMT.
  1135 
  1136 * New commands to load and prove verification conditions generated by
  1137 the Boogie program verifier or derived systems (e.g. the Verifying C
  1138 Compiler (VCC) or Spec#).  See src/HOL/Boogie.
  1139 
  1140 * New counterexample generator tool 'nitpick' based on the Kodkod
  1141 relational model finder.  See src/HOL/Tools/Nitpick and
  1142 src/HOL/Nitpick_Examples.
  1143 
  1144 * New commands 'code_pred' and 'values' to invoke the predicate
  1145 compiler and to enumerate values of inductive predicates.
  1146 
  1147 * A tabled implementation of the reflexive transitive closure.
  1148 
  1149 * New implementation of quickcheck uses generic code generator;
  1150 default generators are provided for all suitable HOL types, records
  1151 and datatypes.  Old quickcheck can be re-activated importing theory
  1152 Library/SML_Quickcheck.
  1153 
  1154 * New testing tool Mirabelle for automated proof tools.  Applies
  1155 several tools and tactics like sledgehammer, metis, or quickcheck, to
  1156 every proof step in a theory.  To be used in batch mode via the
  1157 "mirabelle" utility.
  1158 
  1159 * New proof method "sos" (sum of squares) for nonlinear real
  1160 arithmetic (originally due to John Harison). It requires theory
  1161 Library/Sum_Of_Squares.  It is not a complete decision procedure but
  1162 works well in practice on quantifier-free real arithmetic with +, -,
  1163 *, ^, =, <= and <, i.e. boolean combinations of equalities and
  1164 inequalities between polynomials.  It makes use of external
  1165 semidefinite programming solvers.  Method "sos" generates a
  1166 certificate that can be pasted into the proof thus avoiding the need
  1167 to call an external tool every time the proof is checked.  See
  1168 src/HOL/Library/Sum_Of_Squares.
  1169 
  1170 * New method "linarith" invokes existing linear arithmetic decision
  1171 procedure only.
  1172 
  1173 * New command 'atp_minimal' reduces result produced by Sledgehammer.
  1174 
  1175 * New Sledgehammer option "Full Types" in Proof General settings menu.
  1176 Causes full type information to be output to the ATPs.  This slows
  1177 ATPs down considerably but eliminates a source of unsound "proofs"
  1178 that fail later.
  1179 
  1180 * New method "metisFT": A version of metis that uses full type
  1181 information in order to avoid failures of proof reconstruction.
  1182 
  1183 * New evaluator "approximate" approximates an real valued term using
  1184 the same method as the approximation method.
  1185 
  1186 * Method "approximate" now supports arithmetic expressions as
  1187 boundaries of intervals and implements interval splitting and Taylor
  1188 series expansion.
  1189 
  1190 * ML antiquotation @{code_datatype} inserts definition of a datatype
  1191 generated by the code generator; e.g. see src/HOL/Predicate.thy.
  1192 
  1193 * New theory SupInf of the supremum and infimum operators for sets of
  1194 reals.
  1195 
  1196 * New theory Probability, which contains a development of measure
  1197 theory, eventually leading to Lebesgue integration and probability.
  1198 
  1199 * Extended Multivariate Analysis to include derivation and Brouwer's
  1200 fixpoint theorem.
  1201 
  1202 * Reorganization of number theory, INCOMPATIBILITY:
  1203   - new number theory development for nat and int, in theories Divides
  1204     and GCD as well as in new session Number_Theory
  1205   - some constants and facts now suffixed with _nat and _int
  1206     accordingly
  1207   - former session NumberTheory now named Old_Number_Theory, including
  1208     theories Legacy_GCD and Primes (prefer Number_Theory if possible)
  1209   - moved theory Pocklington from src/HOL/Library to
  1210     src/HOL/Old_Number_Theory
  1211 
  1212 * Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
  1213 lcm of finite and infinite sets. It is shown that they form a complete
  1214 lattice.
  1215 
  1216 * Class semiring_div requires superclass no_zero_divisors and proof of
  1217 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
  1218 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
  1219 generalized to class semiring_div, subsuming former theorems
  1220 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
  1221 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
  1222 INCOMPATIBILITY.
  1223 
  1224 * Refinements to lattice classes and sets:
  1225   - less default intro/elim rules in locale variant, more default
  1226     intro/elim rules in class variant: more uniformity
  1227   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
  1228     le_inf_iff
  1229   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
  1230     sup_aci)
  1231   - renamed ACI to inf_sup_aci
  1232   - new class "boolean_algebra"
  1233   - class "complete_lattice" moved to separate theory
  1234     "Complete_Lattice"; corresponding constants (and abbreviations)
  1235     renamed and with authentic syntax:
  1236     Set.Inf ~>    Complete_Lattice.Inf
  1237     Set.Sup ~>    Complete_Lattice.Sup
  1238     Set.INFI ~>   Complete_Lattice.INFI
  1239     Set.SUPR ~>   Complete_Lattice.SUPR
  1240     Set.Inter ~>  Complete_Lattice.Inter
  1241     Set.Union ~>  Complete_Lattice.Union
  1242     Set.INTER ~>  Complete_Lattice.INTER
  1243     Set.UNION ~>  Complete_Lattice.UNION
  1244   - authentic syntax for
  1245     Set.Pow
  1246     Set.image
  1247   - mere abbreviations:
  1248     Set.empty               (for bot)
  1249     Set.UNIV                (for top)
  1250     Set.inter               (for inf, formerly Set.Int)
  1251     Set.union               (for sup, formerly Set.Un)
  1252     Complete_Lattice.Inter  (for Inf)
  1253     Complete_Lattice.Union  (for Sup)
  1254     Complete_Lattice.INTER  (for INFI)
  1255     Complete_Lattice.UNION  (for SUPR)
  1256   - object-logic definitions as far as appropriate
  1257 
  1258 INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
  1259 Un_subset_iff are explicitly deleted as default simp rules; then also
  1260 their lattice counterparts le_inf_iff and le_sup_iff have to be
  1261 deleted to achieve the desired effect.
  1262 
  1263 * Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
  1264 rules by default any longer; the same applies to min_max.inf_absorb1
  1265 etc.  INCOMPATIBILITY.
  1266 
  1267 * Rules sup_Int_eq and sup_Un_eq are no longer declared as
  1268 pred_set_conv by default.  INCOMPATIBILITY.
  1269 
  1270 * Power operations on relations and functions are now one dedicated
  1271 constant "compow" with infix syntax "^^".  Power operation on
  1272 multiplicative monoids retains syntax "^" and is now defined generic
  1273 in class power.  INCOMPATIBILITY.
  1274 
  1275 * Relation composition "R O S" now has a more standard argument order:
  1276 "R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,
  1277 rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
  1278 break, since the O_assoc rule was not rewritten like this.  Fix using
  1279 O_assoc[symmetric].  The same applies to the curried version "R OO S".
  1280 
  1281 * Function "Inv" is renamed to "inv_into" and function "inv" is now an
  1282 abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
  1283 INCOMPATIBILITY.
  1284 
  1285 * Most rules produced by inductive and datatype package have mandatory
  1286 prefixes.  INCOMPATIBILITY.
  1287 
  1288 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by
  1289 the attribute of the same name.  Each of the theorems in the list
  1290 DERIV_intros assumes composition with an additional function and
  1291 matches a variable to the derivative, which has to be solved by the
  1292 Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
  1293 of most elementary terms.  Former Maclauren.DERIV_tac and
  1294 Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
  1295 INCOMPATIBILITY.
  1296 
  1297 * Code generator attributes follow the usual underscore convention:
  1298     code_unfold     replaces    code unfold
  1299     code_post       replaces    code post
  1300     etc.
  1301   INCOMPATIBILITY.
  1302 
  1303 * Renamed methods:
  1304     sizechange -> size_change
  1305     induct_scheme -> induction_schema
  1306   INCOMPATIBILITY.
  1307 
  1308 * Discontinued abbreviation "arbitrary" of constant "undefined".
  1309 INCOMPATIBILITY, use "undefined" directly.
  1310 
  1311 * Renamed theorems:
  1312     Suc_eq_add_numeral_1 -> Suc_eq_plus1
  1313     Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
  1314     Suc_plus1 -> Suc_eq_plus1
  1315     *anti_sym -> *antisym*
  1316     vector_less_eq_def -> vector_le_def
  1317   INCOMPATIBILITY.
  1318 
  1319 * Added theorem List.map_map as [simp].  Removed List.map_compose.
  1320 INCOMPATIBILITY.
  1321 
  1322 * Removed predicate "M hassize n" (<--> card M = n & finite M).
  1323 INCOMPATIBILITY.
  1324 
  1325 
  1326 *** HOLCF ***
  1327 
  1328 * Theory Representable defines a class "rep" of domains that are
  1329 representable (via an ep-pair) in the universal domain type "udom".
  1330 Instances are provided for all type constructors defined in HOLCF.
  1331 
  1332 * The 'new_domain' command is a purely definitional version of the
  1333 domain package, for representable domains.  Syntax is identical to the
  1334 old domain package.  The 'new_domain' package also supports indirect
  1335 recursion using previously-defined type constructors.  See
  1336 src/HOLCF/ex/New_Domain.thy for examples.
  1337 
  1338 * Method "fixrec_simp" unfolds one step of a fixrec-defined constant
  1339 on the left-hand side of an equation, and then performs
  1340 simplification.  Rewriting is done using rules declared with the
  1341 "fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
  1342 replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
  1343 
  1344 * The pattern-match compiler in 'fixrec' can now handle constructors
  1345 with HOL function types.  Pattern-match combinators for the Pair
  1346 constructor are pre-configured.
  1347 
  1348 * The 'fixrec' package now produces better fixed-point induction rules
  1349 for mutually-recursive definitions:  Induction rules have conclusions
  1350 of the form "P foo bar" instead of "P <foo, bar>".
  1351 
  1352 * The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
  1353 been renamed to "below".  The name "below" now replaces "less" in many
  1354 theorem names.  (Legacy theorem names using "less" are still supported
  1355 as well.)
  1356 
  1357 * The 'fixrec' package now supports "bottom patterns".  Bottom
  1358 patterns can be used to generate strictness rules, or to make
  1359 functions more strict (much like the bang-patterns supported by the
  1360 Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
  1361 examples.
  1362 
  1363 
  1364 *** ML ***
  1365 
  1366 * Support for Poly/ML 5.3.0, with improved reporting of compiler
  1367 errors and run-time exceptions, including detailed source positions.
  1368 
  1369 * Structure Name_Space (formerly NameSpace) now manages uniquely
  1370 identified entries, with some additional information such as source
  1371 position, logical grouping etc.
  1372 
  1373 * Theory and context data is now introduced by the simplified and
  1374 modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
  1375 to be pure, but the old TheoryDataFun for mutable data (with explicit
  1376 copy operation) is still available for some time.
  1377 
  1378 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
  1379 provides a high-level programming interface to synchronized state
  1380 variables with atomic update.  This works via pure function
  1381 application within a critical section -- its runtime should be as
  1382 short as possible; beware of deadlocks if critical code is nested,
  1383 either directly or indirectly via other synchronized variables!
  1384 
  1385 * Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
  1386 wraps raw ML references, explicitly indicating their non-thread-safe
  1387 behaviour.  The Isar toplevel keeps this structure open, to
  1388 accommodate Proof General as well as quick and dirty interactive
  1389 experiments with references.
  1390 
  1391 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
  1392 parallel tactical reasoning.
  1393 
  1394 * Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
  1395 are similar to SUBPROOF, but are slightly more flexible: only the
  1396 specified parts of the subgoal are imported into the context, and the
  1397 body tactic may introduce new subgoals and schematic variables.
  1398 
  1399 * Old tactical METAHYPS, which does not observe the proof context, has
  1400 been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
  1401 or Subgoal.FOCUS etc.
  1402 
  1403 * Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
  1404 functors have their own ML name space there is no point to mark them
  1405 separately.)  Minor INCOMPATIBILITY.
  1406 
  1407 * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
  1408 
  1409 * Renamed several structures FooBar to Foo_Bar.  Occasional,
  1410 INCOMPATIBILITY.
  1411 
  1412 * Operations of structure Skip_Proof no longer require quick_and_dirty
  1413 mode, which avoids critical setmp.
  1414 
  1415 * Eliminated old Attrib.add_attributes, Method.add_methods and related
  1416 combinators for "args".  INCOMPATIBILITY, need to use simplified
  1417 Attrib/Method.setup introduced in Isabelle2009.
  1418 
  1419 * Proper context for simpset_of, claset_of, clasimpset_of.  May fall
  1420 back on global_simpset_of, global_claset_of, global_clasimpset_of as
  1421 last resort.  INCOMPATIBILITY.
  1422 
  1423 * Display.pretty_thm now requires a proper context (cf. former
  1424 ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
  1425 or even Display.pretty_thm_without_context as last resort.
  1426 INCOMPATIBILITY.
  1427 
  1428 * Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
  1429 Syntax.pretty_typ/term directly, preferably with proper context
  1430 instead of global theory.
  1431 
  1432 
  1433 *** System ***
  1434 
  1435 * Further fine tuning of parallel proof checking, scales up to 8 cores
  1436 (max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and
  1437 usedir option -q.
  1438 
  1439 * Support for additional "Isabelle components" via etc/components, see
  1440 also the system manual.
  1441 
  1442 * The isabelle makeall tool now operates on all components with
  1443 IsaMakefile, not just hardwired "logics".
  1444 
  1445 * Removed "compress" option from isabelle-process and isabelle usedir;
  1446 this is always enabled.
  1447 
  1448 * Discontinued support for Poly/ML 4.x versions.
  1449 
  1450 * Isabelle tool "wwwfind" provides web interface for 'find_theorems'
  1451 on a given logic image.  This requires the lighttpd webserver and is
  1452 currently supported on Linux only.
  1453 
  1454 
  1455 
  1456 New in Isabelle2009 (April 2009)
  1457 --------------------------------
  1458 
  1459 *** General ***
  1460 
  1461 * Simplified main Isabelle executables, with less surprises on
  1462 case-insensitive file-systems (such as Mac OS).
  1463 
  1464   - The main Isabelle tool wrapper is now called "isabelle" instead of
  1465     "isatool."
  1466 
  1467   - The former "isabelle" alias for "isabelle-process" has been
  1468     removed (should rarely occur to regular users).
  1469 
  1470   - The former "isabelle-interface" and its alias "Isabelle" have been
  1471     removed (interfaces are now regular Isabelle tools).
  1472 
  1473 Within scripts and make files, the Isabelle environment variables
  1474 ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
  1475 respectively.  (The latter are still available as legacy feature.)
  1476 
  1477 The old isabelle-interface wrapper could react in confusing ways if
  1478 the interface was uninstalled or changed otherwise.  Individual
  1479 interface tool configuration is now more explicit, see also the
  1480 Isabelle system manual.  In particular, Proof General is now available
  1481 via "isabelle emacs".
  1482 
  1483 INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to
  1484 purge installed copies of Isabelle executables and re-run "isabelle
  1485 install -p ...", or use symlinks.
  1486 
  1487 * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
  1488 old ~/isabelle, which was slightly non-standard and apt to cause
  1489 surprises on case-insensitive file-systems (such as Mac OS).
  1490 
  1491 INCOMPATIBILITY, need to move existing ~/isabelle/etc,
  1492 ~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special
  1493 care is required when using older releases of Isabelle.  Note that
  1494 ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
  1495 Isabelle distribution, in order to use the new ~/.isabelle uniformly.
  1496 
  1497 * Proofs of fully specified statements are run in parallel on
  1498 multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on
  1499 a regular 4-core machine, if the initial heap space is made reasonably
  1500 large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)
  1501 
  1502 * The main reference manuals ("isar-ref", "implementation", and
  1503 "system") have been updated and extended.  Formally checked references
  1504 as hyperlinks are now available uniformly.
  1505 
  1506 
  1507 *** Pure ***
  1508 
  1509 * Complete re-implementation of locales.  INCOMPATIBILITY in several
  1510 respects.  The most important changes are listed below.  See the
  1511 Tutorial on Locales ("locales" manual) for details.
  1512 
  1513 - In locale expressions, instantiation replaces renaming.  Parameters
  1514 must be declared in a for clause.  To aid compatibility with previous
  1515 parameter inheritance, in locale declarations, parameters that are not
  1516 'touched' (instantiation position "_" or omitted) are implicitly added
  1517 with their syntax at the beginning of the for clause.
  1518 
  1519 - Syntax from abbreviations and definitions in locales is available in
  1520 locale expressions and context elements.  The latter is particularly
  1521 useful in locale declarations.
  1522 
  1523 - More flexible mechanisms to qualify names generated by locale
  1524 expressions.  Qualifiers (prefixes) may be specified in locale
  1525 expressions, and can be marked as mandatory (syntax: "name!:") or
  1526 optional (syntax "name?:").  The default depends for plain "name:"
  1527 depends on the situation where a locale expression is used: in
  1528 commands 'locale' and 'sublocale' prefixes are optional, in
  1529 'interpretation' and 'interpret' prefixes are mandatory.  The old
  1530 implicit qualifiers derived from the parameter names of a locale are
  1531 no longer generated.
  1532 
  1533 - Command "sublocale l < e" replaces "interpretation l < e".  The
  1534 instantiation clause in "interpretation" and "interpret" (square
  1535 brackets) is no longer available.  Use locale expressions.
  1536 
  1537 - When converting proof scripts, mandatory qualifiers in
  1538 'interpretation' and 'interpret' should be retained by default, even
  1539 if this is an INCOMPATIBILITY compared to former behavior.  In the
  1540 worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
  1541 in locale expressions range over a single locale instance only.
  1542 
  1543 - Dropped locale element "includes".  This is a major INCOMPATIBILITY.
  1544 In existing theorem specifications replace the includes element by the
  1545 respective context elements of the included locale, omitting those
  1546 that are already present in the theorem specification.  Multiple
  1547 assume elements of a locale should be replaced by a single one
  1548 involving the locale predicate.  In the proof body, declarations (most
  1549 notably theorems) may be regained by interpreting the respective
  1550 locales in the proof context as required (command "interpret").
  1551 
  1552 If using "includes" in replacement of a target solely because the
  1553 parameter types in the theorem are not as general as in the target,
  1554 consider declaring a new locale with additional type constraints on
  1555 the parameters (context element "constrains").
  1556 
  1557 - Discontinued "locale (open)".  INCOMPATIBILITY.
  1558 
  1559 - Locale interpretation commands no longer attempt to simplify goal.
  1560 INCOMPATIBILITY: in rare situations the generated goal differs.  Use
  1561 methods intro_locales and unfold_locales to clarify.
  1562 
  1563 - Locale interpretation commands no longer accept interpretation
  1564 attributes.  INCOMPATIBILITY.
  1565 
  1566 * Class declaration: so-called "base sort" must not be given in import
  1567 list any longer, but is inferred from the specification.  Particularly
  1568 in HOL, write
  1569 
  1570     class foo = ...
  1571 
  1572 instead of
  1573 
  1574     class foo = type + ...
  1575 
  1576 * Class target: global versions of theorems stemming do not carry a
  1577 parameter prefix any longer.  INCOMPATIBILITY.
  1578 
  1579 * Class 'instance' command no longer accepts attached definitions.
  1580 INCOMPATIBILITY, use proper 'instantiation' target instead.
  1581 
  1582 * Recovered hiding of consts, which was accidentally broken in
  1583 Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
  1584 makes c inaccessible; consider using ``hide (open) const c'' instead.
  1585 
  1586 * Slightly more coherent Pure syntax, with updated documentation in
  1587 isar-ref manual.  Removed locales meta_term_syntax and
  1588 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
  1589 INCOMPATIBILITY in rare situations.  Note that &&& should not be used
  1590 directly in regular applications.
  1591 
  1592 * There is a new syntactic category "float_const" for signed decimal
  1593 fractions (e.g. 123.45 or -123.45).
  1594 
  1595 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
  1596 interface with 'setup' command instead.
  1597 
  1598 * Command 'local_setup' is similar to 'setup', but operates on a local
  1599 theory context.
  1600 
  1601 * The 'axiomatization' command now only works within a global theory
  1602 context.  INCOMPATIBILITY.
  1603 
  1604 * Goal-directed proof now enforces strict proof irrelevance wrt. sort
  1605 hypotheses.  Sorts required in the course of reasoning need to be
  1606 covered by the constraints in the initial statement, completed by the
  1607 type instance information of the background theory.  Non-trivial sort
  1608 hypotheses, which rarely occur in practice, may be specified via
  1609 vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
  1610 
  1611   lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
  1612 
  1613 The result contains an implicit sort hypotheses as before --
  1614 SORT_CONSTRAINT premises are eliminated as part of the canonical rule
  1615 normalization.
  1616 
  1617 * Generalized Isar history, with support for linear undo, direct state
  1618 addressing etc.
  1619 
  1620 * Changed defaults for unify configuration options:
  1621 
  1622   unify_trace_bound = 50 (formerly 25)
  1623   unify_search_bound = 60 (formerly 30)
  1624 
  1625 * Different bookkeeping for code equations (INCOMPATIBILITY):
  1626 
  1627   a) On theory merge, the last set of code equations for a particular
  1628      constant is taken (in accordance with the policy applied by other
  1629      parts of the code generator framework).
  1630 
  1631   b) Code equations stemming from explicit declarations (e.g. code
  1632      attribute) gain priority over default code equations stemming
  1633      from definition, primrec, fun etc.
  1634 
  1635 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
  1636 
  1637 * Unified theorem tables for both code generators.  Thus [code
  1638 func] has disappeared and only [code] remains.  INCOMPATIBILITY.
  1639 
  1640 * Command 'find_consts' searches for constants based on type and name
  1641 patterns, e.g.
  1642 
  1643     find_consts "_ => bool"
  1644 
  1645 By default, matching is against subtypes, but it may be restricted to
  1646 the whole type.  Searching by name is possible.  Multiple queries are
  1647 conjunctive and queries may be negated by prefixing them with a
  1648 hyphen:
  1649 
  1650     find_consts strict: "_ => bool" name: "Int" -"int => int"
  1651 
  1652 * New 'find_theorems' criterion "solves" matches theorems that
  1653 directly solve the current goal (modulo higher-order unification).
  1654 
  1655 * Auto solve feature for main theorem statements: whenever a new goal
  1656 is stated, "find_theorems solves" is called; any theorems that could
  1657 solve the lemma directly are listed as part of the goal state.
  1658 Cf. associated options in Proof General Isabelle settings menu,
  1659 enabled by default, with reasonable timeout for pathological cases of
  1660 higher-order unification.
  1661 
  1662 
  1663 *** Document preparation ***
  1664 
  1665 * Antiquotation @{lemma} now imitates a regular terminal proof,
  1666 demanding keyword 'by' and supporting the full method expression
  1667 syntax just like the Isar command 'by'.
  1668 
  1669 
  1670 *** HOL ***
  1671 
  1672 * Integrated main parts of former image HOL-Complex with HOL.  Entry
  1673 points Main and Complex_Main remain as before.
  1674 
  1675 * Logic image HOL-Plain provides a minimal HOL with the most important
  1676 tools available (inductive, datatype, primrec, ...).  This facilitates
  1677 experimentation and tool development.  Note that user applications
  1678 (and library theories) should never refer to anything below theory
  1679 Main, as before.
  1680 
  1681 * Logic image HOL-Main stops at theory Main, and thus facilitates
  1682 experimentation due to shorter build times.
  1683 
  1684 * Logic image HOL-NSA contains theories of nonstandard analysis which
  1685 were previously part of former HOL-Complex.  Entry point Hyperreal
  1686 remains valid, but theories formerly using Complex_Main should now use
  1687 new entry point Hypercomplex.
  1688 
  1689 * Generic ATP manager for Sledgehammer, based on ML threads instead of
  1690 Posix processes.  Avoids potentially expensive forking of the ML
  1691 process.  New thread-based implementation also works on non-Unix
  1692 platforms (Cygwin).  Provers are no longer hardwired, but defined
  1693 within the theory via plain ML wrapper functions.  Basic Sledgehammer
  1694 commands are covered in the isar-ref manual.
  1695 
  1696 * Wrapper scripts for remote SystemOnTPTP service allows to use
  1697 sledgehammer without local ATP installation (Vampire etc.). Other
  1698 provers may be included via suitable ML wrappers, see also
  1699 src/HOL/ATP_Linkup.thy.
  1700 
  1701 * ATP selection (E/Vampire/Spass) is now via Proof General's settings
  1702 menu.
  1703 
  1704 * The metis method no longer fails because the theorem is too trivial
  1705 (contains the empty clause).
  1706 
  1707 * The metis method now fails in the usual manner, rather than raising
  1708 an exception, if it determines that it cannot prove the theorem.
  1709 
  1710 * Method "coherent" implements a prover for coherent logic (see also
  1711 src/Tools/coherent.ML).
  1712 
  1713 * Constants "undefined" and "default" replace "arbitrary".  Usually
  1714 "undefined" is the right choice to replace "arbitrary", though
  1715 logically there is no difference.  INCOMPATIBILITY.
  1716 
  1717 * Command "value" now integrates different evaluation mechanisms.  The
  1718 result of the first successful evaluation mechanism is printed.  In
  1719 square brackets a particular named evaluation mechanisms may be
  1720 specified (currently, [SML], [code] or [nbe]).  See further
  1721 src/HOL/ex/Eval_Examples.thy.
  1722 
  1723 * Normalization by evaluation now allows non-leftlinear equations.
  1724 Declare with attribute [code nbe].
  1725 
  1726 * Methods "case_tac" and "induct_tac" now refer to the very same rules
  1727 as the structured Isar versions "cases" and "induct", cf. the
  1728 corresponding "cases" and "induct" attributes.  Mutual induction rules
  1729 are now presented as a list of individual projections
  1730 (e.g. foo_bar.inducts for types foo and bar); the old format with
  1731 explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
  1732 rare situations a different rule is selected --- notably nested tuple
  1733 elimination instead of former prod.exhaust: use explicit (case_tac t
  1734 rule: prod.exhaust) here.
  1735 
  1736 * Attributes "cases", "induct", "coinduct" support "del" option.
  1737 
  1738 * Removed fact "case_split_thm", which duplicates "case_split".
  1739 
  1740 * The option datatype has been moved to a new theory Option.  Renamed
  1741 option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.
  1742 
  1743 * New predicate "strict_mono" classifies strict functions on partial
  1744 orders.  With strict functions on linear orders, reasoning about
  1745 (in)equalities is facilitated by theorems "strict_mono_eq",
  1746 "strict_mono_less_eq" and "strict_mono_less".
  1747 
  1748 * Some set operations are now proper qualified constants with
  1749 authentic syntax.  INCOMPATIBILITY:
  1750 
  1751     op Int ~>   Set.Int
  1752     op Un ~>    Set.Un
  1753     INTER ~>    Set.INTER
  1754     UNION ~>    Set.UNION
  1755     Inter ~>    Set.Inter
  1756     Union ~>    Set.Union
  1757     {} ~>       Set.empty
  1758     UNIV ~>     Set.UNIV
  1759 
  1760 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in
  1761 theory Set.
  1762 
  1763 * Auxiliary class "itself" has disappeared -- classes without any
  1764 parameter are treated as expected by the 'class' command.
  1765 
  1766 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
  1767 
  1768 * Common decision procedures (Cooper, MIR, Ferrack, Approximation,
  1769 Dense_Linear_Order) are now in directory HOL/Decision_Procs.
  1770 
  1771 * Theory src/HOL/Decision_Procs/Approximation provides the new proof
  1772 method "approximation".  It proves formulas on real values by using
  1773 interval arithmetic.  In the formulas are also the transcendental
  1774 functions sin, cos, tan, atan, ln, exp and the constant pi are
  1775 allowed. For examples see
  1776 src/HOL/Descision_Procs/ex/Approximation_Ex.thy.
  1777 
  1778 * Theory "Reflection" now resides in HOL/Library.
  1779 
  1780 * Entry point to Word library now simply named "Word".
  1781 INCOMPATIBILITY.
  1782 
  1783 * Made source layout more coherent with logical distribution
  1784 structure:
  1785 
  1786     src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
  1787     src/HOL/Library/Code_Message.thy ~> src/HOL/
  1788     src/HOL/Library/GCD.thy ~> src/HOL/
  1789     src/HOL/Library/Order_Relation.thy ~> src/HOL/
  1790     src/HOL/Library/Parity.thy ~> src/HOL/
  1791     src/HOL/Library/Univ_Poly.thy ~> src/HOL/
  1792     src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/
  1793     src/HOL/Real/Lubs.thy ~> src/HOL/
  1794     src/HOL/Real/PReal.thy ~> src/HOL/
  1795     src/HOL/Real/Rational.thy ~> src/HOL/
  1796     src/HOL/Real/RComplete.thy ~> src/HOL/
  1797     src/HOL/Real/RealDef.thy ~> src/HOL/
  1798     src/HOL/Real/RealPow.thy ~> src/HOL/
  1799     src/HOL/Real/Real.thy ~> src/HOL/
  1800     src/HOL/Complex/Complex_Main.thy ~> src/HOL/
  1801     src/HOL/Complex/Complex.thy ~> src/HOL/
  1802     src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/
  1803     src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/
  1804     src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
  1805     src/HOL/Hyperreal/Fact.thy ~> src/HOL/
  1806     src/HOL/Hyperreal/Integration.thy ~> src/HOL/
  1807     src/HOL/Hyperreal/Lim.thy ~> src/HOL/
  1808     src/HOL/Hyperreal/Ln.thy ~> src/HOL/
  1809     src/HOL/Hyperreal/Log.thy ~> src/HOL/
  1810     src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/
  1811     src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/
  1812     src/HOL/Hyperreal/Series.thy ~> src/HOL/
  1813     src/HOL/Hyperreal/SEQ.thy ~> src/HOL/
  1814     src/HOL/Hyperreal/Taylor.thy ~> src/HOL/
  1815     src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/
  1816     src/HOL/Real/Float ~> src/HOL/Library/
  1817     src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach
  1818     src/HOL/Real/RealVector.thy ~> src/HOL/
  1819 
  1820     src/HOL/arith_data.ML ~> src/HOL/Tools
  1821     src/HOL/hologic.ML ~> src/HOL/Tools
  1822     src/HOL/simpdata.ML ~> src/HOL/Tools
  1823     src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML
  1824     src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools
  1825     src/HOL/nat_simprocs.ML ~> src/HOL/Tools
  1826     src/HOL/Real/float_arith.ML ~> src/HOL/Tools
  1827     src/HOL/Real/float_syntax.ML ~> src/HOL/Tools
  1828     src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
  1829     src/HOL/Real/real_arith.ML ~> src/HOL/Tools
  1830 
  1831     src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
  1832     src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
  1833     src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
  1834     src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
  1835     src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
  1836     src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
  1837 
  1838 * If methods "eval" and "evaluation" encounter a structured proof
  1839 state with !!/==>, only the conclusion is evaluated to True (if
  1840 possible), avoiding strange error messages.
  1841 
  1842 * Method "sizechange" automates termination proofs using (a
  1843 modification of) the size-change principle.  Requires SAT solver.  See
  1844 src/HOL/ex/Termination.thy for examples.
  1845 
  1846 * Simplifier: simproc for let expressions now unfolds if bound
  1847 variable occurs at most once in let expression body.  INCOMPATIBILITY.
  1848 
  1849 * Method "arith": Linear arithmetic now ignores all inequalities when
  1850 fast_arith_neq_limit is exceeded, instead of giving up entirely.
  1851 
  1852 * New attribute "arith" for facts that should always be used
  1853 automatically by arithmetic. It is intended to be used locally in
  1854 proofs, e.g.
  1855 
  1856   assumes [arith]: "x > 0"
  1857 
  1858 Global usage is discouraged because of possible performance impact.
  1859 
  1860 * New classes "top" and "bot" with corresponding operations "top" and
  1861 "bot" in theory Orderings; instantiation of class "complete_lattice"
  1862 requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.
  1863 
  1864 * Changed definition lemma "less_fun_def" in order to provide an
  1865 instance for preorders on functions; use lemma "less_le" instead.
  1866 INCOMPATIBILITY.
  1867 
  1868 * Theory Orderings: class "wellorder" moved here, with explicit
  1869 induction rule "less_induct" as assumption.  For instantiation of
  1870 "wellorder" by means of predicate "wf", use rule wf_wellorderI.
  1871 INCOMPATIBILITY.
  1872 
  1873 * Theory Orderings: added class "preorder" as superclass of "order".
  1874 INCOMPATIBILITY: Instantiation proofs for order, linorder
  1875 etc. slightly changed.  Some theorems named order_class.* now named
  1876 preorder_class.*.
  1877 
  1878 * Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,
  1879 "diag" to "Id_on".
  1880 
  1881 * Theory Finite_Set: added a new fold combinator of type
  1882 
  1883   ('a => 'b => 'b) => 'b => 'a set => 'b
  1884 
  1885 Occasionally this is more convenient than the old fold combinator
  1886 which is now defined in terms of the new one and renamed to
  1887 fold_image.
  1888 
  1889 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"
  1890 and "ring_simps" have been replaced by "algebra_simps" (which can be
  1891 extended with further lemmas!).  At the moment both still exist but
  1892 the former will disappear at some point.
  1893 
  1894 * Theory Power: Lemma power_Suc is now declared as a simp rule in
  1895 class recpower.  Type-specific simp rules for various recpower types
  1896 have been removed.  INCOMPATIBILITY, rename old lemmas as follows:
  1897 
  1898 rat_power_0    -> power_0
  1899 rat_power_Suc  -> power_Suc
  1900 realpow_0      -> power_0
  1901 realpow_Suc    -> power_Suc
  1902 complexpow_0   -> power_0
  1903 complexpow_Suc -> power_Suc
  1904 power_poly_0   -> power_0
  1905 power_poly_Suc -> power_Suc
  1906 
  1907 * Theories Ring_and_Field and Divides: Definition of "op dvd" has been
  1908 moved to separate class dvd in Ring_and_Field; a couple of lemmas on
  1909 dvd has been generalized to class comm_semiring_1.  Likewise a bunch
  1910 of lemmas from Divides has been generalized from nat to class
  1911 semiring_div.  INCOMPATIBILITY.  This involves the following theorem
  1912 renames resulting from duplicate elimination:
  1913 
  1914     dvd_def_mod ~>          dvd_eq_mod_eq_0
  1915     zero_dvd_iff ~>         dvd_0_left_iff
  1916     dvd_0 ~>                dvd_0_right
  1917     DIVISION_BY_ZERO_DIV ~> div_by_0
  1918     DIVISION_BY_ZERO_MOD ~> mod_by_0
  1919     mult_div ~>             div_mult_self2_is_id
  1920     mult_mod ~>             mod_mult_self2_is_0
  1921 
  1922 * Theory IntDiv: removed many lemmas that are instances of class-based
  1923 generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,
  1924 rename old lemmas as follows:
  1925 
  1926 dvd_diff               -> nat_dvd_diff
  1927 dvd_zminus_iff         -> dvd_minus_iff
  1928 mod_add1_eq            -> mod_add_eq
  1929 mod_mult1_eq           -> mod_mult_right_eq
  1930 mod_mult1_eq'          -> mod_mult_left_eq
  1931 mod_mult_distrib_mod   -> mod_mult_eq
  1932 nat_mod_add_left_eq    -> mod_add_left_eq
  1933 nat_mod_add_right_eq   -> mod_add_right_eq
  1934 nat_mod_div_trivial    -> mod_div_trivial
  1935 nat_mod_mod_trivial    -> mod_mod_trivial
  1936 zdiv_zadd_self1        -> div_add_self1
  1937 zdiv_zadd_self2        -> div_add_self2
  1938 zdiv_zmult_self1       -> div_mult_self2_is_id
  1939 zdiv_zmult_self2       -> div_mult_self1_is_id
  1940 zdvd_triv_left         -> dvd_triv_left
  1941 zdvd_triv_right        -> dvd_triv_right
  1942 zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
  1943 zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]
  1944 zmod_zadd_left_eq      -> mod_add_left_eq
  1945 zmod_zadd_right_eq     -> mod_add_right_eq
  1946 zmod_zadd_self1        -> mod_add_self1
  1947 zmod_zadd_self2        -> mod_add_self2
  1948 zmod_zadd1_eq          -> mod_add_eq
  1949 zmod_zdiff1_eq         -> mod_diff_eq
  1950 zmod_zdvd_zmod         -> mod_mod_cancel
  1951 zmod_zmod_cancel       -> mod_mod_cancel
  1952 zmod_zmult_self1       -> mod_mult_self2_is_0
  1953 zmod_zmult_self2       -> mod_mult_self1_is_0
  1954 zmod_1                 -> mod_by_1
  1955 zdiv_1                 -> div_by_1
  1956 zdvd_abs1              -> abs_dvd_iff
  1957 zdvd_abs2              -> dvd_abs_iff
  1958 zdvd_refl              -> dvd_refl
  1959 zdvd_trans             -> dvd_trans
  1960 zdvd_zadd              -> dvd_add
  1961 zdvd_zdiff             -> dvd_diff
  1962 zdvd_zminus_iff        -> dvd_minus_iff
  1963 zdvd_zminus2_iff       -> minus_dvd_iff
  1964 zdvd_zmultD            -> dvd_mult_right
  1965 zdvd_zmultD2           -> dvd_mult_left
  1966 zdvd_zmult_mono        -> mult_dvd_mono
  1967 zdvd_0_right           -> dvd_0_right
  1968 zdvd_0_left            -> dvd_0_left_iff
  1969 zdvd_1_left            -> one_dvd
  1970 zminus_dvd_iff         -> minus_dvd_iff
  1971 
  1972 * Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
  1973 
  1974 * The real numbers offer decimal input syntax: 12.34 is translated
  1975 into 1234/10^2. This translation is not reversed upon output.
  1976 
  1977 * Theory Library/Polynomial defines an abstract type 'a poly of
  1978 univariate polynomials with coefficients of type 'a.  In addition to
  1979 the standard ring operations, it also supports div and mod.  Code
  1980 generation is also supported, using list-style constructors.
  1981 
  1982 * Theory Library/Inner_Product defines a class of real_inner for real
  1983 inner product spaces, with an overloaded operation inner :: 'a => 'a
  1984 => real.  Class real_inner is a subclass of real_normed_vector from
  1985 theory RealVector.
  1986 
  1987 * Theory Library/Product_Vector provides instances for the product
  1988 type 'a * 'b of several classes from RealVector and Inner_Product.
  1989 Definitions of addition, subtraction, scalar multiplication, norms,
  1990 and inner products are included.
  1991 
  1992 * Theory Library/Bit defines the field "bit" of integers modulo 2.  In
  1993 addition to the field operations, numerals and case syntax are also
  1994 supported.
  1995 
  1996 * Theory Library/Diagonalize provides constructive version of Cantor's
  1997 first diagonalization argument.
  1998 
  1999 * Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
  2000 zlcm (for int); carried together from various gcd/lcm developements in
  2001 the HOL Distribution.  Constants zgcd and zlcm replace former igcd and
  2002 ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,
  2003 may recover tupled syntax as follows:
  2004 
  2005     hide (open) const gcd
  2006     abbreviation gcd where
  2007       "gcd == (%(a, b). GCD.gcd a b)"
  2008     notation (output)
  2009       GCD.gcd ("gcd '(_, _')")
  2010 
  2011 The same works for lcm, zgcd, zlcm.
  2012 
  2013 * Theory Library/Nat_Infinity: added addition, numeral syntax and more
  2014 instantiations for algebraic structures.  Removed some duplicate
  2015 theorems.  Changes in simp rules.  INCOMPATIBILITY.
  2016 
  2017 * ML antiquotation @{code} takes a constant as argument and generates
  2018 corresponding code in background and inserts name of the corresponding
  2019 resulting ML value/function/datatype constructor binding in place.
  2020 All occurrences of @{code} with a single ML block are generated
  2021 simultaneously.  Provides a generic and safe interface for
  2022 instrumentalizing code generation.  See
  2023 src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.
  2024 In future you ought to refrain from ad-hoc compiling generated SML
  2025 code on the ML toplevel.  Note that (for technical reasons) @{code}
  2026 cannot refer to constants for which user-defined serializations are
  2027 set.  Refer to the corresponding ML counterpart directly in that
  2028 cases.
  2029 
  2030 * Command 'rep_datatype': instead of theorem names the command now
  2031 takes a list of terms denoting the constructors of the type to be
  2032 represented as datatype.  The characteristic theorems have to be
  2033 proven.  INCOMPATIBILITY.  Also observe that the following theorems
  2034 have disappeared in favour of existing ones:
  2035 
  2036     unit_induct                 ~> unit.induct
  2037     prod_induct                 ~> prod.induct
  2038     sum_induct                  ~> sum.induct
  2039     Suc_Suc_eq                  ~> nat.inject
  2040     Suc_not_Zero Zero_not_Suc   ~> nat.distinct
  2041 
  2042 
  2043 *** HOL-Algebra ***
  2044 
  2045 * New locales for orders and lattices where the equivalence relation
  2046 is not restricted to equality.  INCOMPATIBILITY: all order and lattice
  2047 locales use a record structure with field eq for the equivalence.
  2048 
  2049 * New theory of factorial domains.
  2050 
  2051 * Units_l_inv and Units_r_inv are now simp rules by default.
  2052 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
  2053 and/or r_inv will now also require deletion of these lemmas.
  2054 
  2055 * Renamed the following theorems, INCOMPATIBILITY:
  2056 
  2057 UpperD ~> Upper_memD
  2058 LowerD ~> Lower_memD
  2059 least_carrier ~> least_closed
  2060 greatest_carrier ~> greatest_closed
  2061 greatest_Lower_above ~> greatest_Lower_below
  2062 one_zero ~> carrier_one_zero
  2063 one_not_zero ~> carrier_one_not_zero  (collision with assumption)
  2064 
  2065 
  2066 *** HOL-Nominal ***
  2067 
  2068 * Nominal datatypes can now contain type-variables.
  2069 
  2070 * Commands 'nominal_inductive' and 'equivariance' work with local
  2071 theory targets.
  2072 
  2073 * Nominal primrec can now works with local theory targets and its
  2074 specification syntax now conforms to the general format as seen in
  2075 'inductive' etc.
  2076 
  2077 * Method "perm_simp" honours the standard simplifier attributes
  2078 (no_asm), (no_asm_use) etc.
  2079 
  2080 * The new predicate #* is defined like freshness, except that on the
  2081 left hand side can be a set or list of atoms.
  2082 
  2083 * Experimental command 'nominal_inductive2' derives strong induction
  2084 principles for inductive definitions.  In contrast to
  2085 'nominal_inductive', which can only deal with a fixed number of
  2086 binders, it can deal with arbitrary expressions standing for sets of
  2087 atoms to be avoided.  The only inductive definition we have at the
  2088 moment that needs this generalisation is the typing rule for Lets in
  2089 the algorithm W:
  2090 
  2091  Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
  2092  -----------------------------------------------------------------
  2093          Gamma |- Let x be t1 in t2 : T2
  2094 
  2095 In this rule one wants to avoid all the binders that are introduced by
  2096 "close Gamma T1".  We are looking for other examples where this
  2097 feature might be useful.  Please let us know.
  2098 
  2099 
  2100 *** HOLCF ***
  2101 
  2102 * Reimplemented the simplification procedure for proving continuity
  2103 subgoals.  The new simproc is extensible; users can declare additional
  2104 continuity introduction rules with the attribute [cont2cont].
  2105 
  2106 * The continuity simproc now uses a different introduction rule for
  2107 solving continuity subgoals on terms with lambda abstractions.  In
  2108 some rare cases the new simproc may fail to solve subgoals that the
  2109 old one could solve, and "simp add: cont2cont_LAM" may be necessary.
  2110 Potential INCOMPATIBILITY.
  2111 
  2112 * Command 'fixrec': specification syntax now conforms to the general
  2113 format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
  2114 examples.  INCOMPATIBILITY.
  2115 
  2116 
  2117 *** ZF ***
  2118 
  2119 * Proof of Zorn's Lemma for partial orders.
  2120 
  2121 
  2122 *** ML ***
  2123 
  2124 * Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
  2125 Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility
  2126 depends on multithreading, so timouts will not work before Poly/ML
  2127 5.2.1!
  2128 
  2129 * High-level support for concurrent ML programming, see
  2130 src/Pure/Cuncurrent.  The data-oriented model of "future values" is
  2131 particularly convenient to organize independent functional
  2132 computations.  The concept of "synchronized variables" provides a
  2133 higher-order interface for components with shared state, avoiding the
  2134 delicate details of mutexes and condition variables.  (Requires
  2135 Poly/ML 5.2.1 or later.)
  2136 
  2137 * ML bindings produced via Isar commands are stored within the Isar
  2138 context (theory or proof).  Consequently, commands like 'use' and 'ML'
  2139 become thread-safe and work with undo as expected (concerning
  2140 top-level bindings, not side-effects on global references).
  2141 INCOMPATIBILITY, need to provide proper Isar context when invoking the
  2142 compiler at runtime; really global bindings need to be given outside a
  2143 theory.  (Requires Poly/ML 5.2 or later.)
  2144 
  2145 * Command 'ML_prf' is analogous to 'ML' but works within a proof
  2146 context.  Top-level ML bindings are stored within the proof context in
  2147 a purely sequential fashion, disregarding the nested proof structure.
  2148 ML bindings introduced by 'ML_prf' are discarded at the end of the
  2149 proof.  (Requires Poly/ML 5.2 or later.)
  2150 
  2151 * Simplified ML attribute and method setup, cf. functions Attrib.setup
  2152 and Method.setup, as well as Isar commands 'attribute_setup' and
  2153 'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify
  2154 existing code accordingly, or use plain 'setup' together with old
  2155 Method.add_method.
  2156 
  2157 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
  2158 to 'a -> thm, while results are always tagged with an authentic oracle
  2159 name.  The Isar command 'oracle' is now polymorphic, no argument type
  2160 is specified.  INCOMPATIBILITY, need to simplify existing oracle code
  2161 accordingly.  Note that extra performance may be gained by producing
  2162 the cterm carefully, avoiding slow Thm.cterm_of.
  2163 
  2164 * Simplified interface for defining document antiquotations via
  2165 ThyOutput.antiquotation, ThyOutput.output, and optionally
  2166 ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
  2167 antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
  2168 examples.
  2169 
  2170 * More systematic treatment of long names, abstract name bindings, and
  2171 name space operations.  Basic operations on qualified names have been
  2172 move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
  2173 Long_Name.append.  Old type bstring has been mostly replaced by
  2174 abstract type binding (see structure Binding), which supports precise
  2175 qualification by packages and local theory targets, as well as proper
  2176 tracking of source positions.  INCOMPATIBILITY, need to wrap old
  2177 bstring values into Binding.name, or better pass through abstract
  2178 bindings everywhere.  See further src/Pure/General/long_name.ML,
  2179 src/Pure/General/binding.ML and src/Pure/General/name_space.ML
  2180 
  2181 * Result facts (from PureThy.note_thms, ProofContext.note_thms,
  2182 LocalTheory.note etc.) now refer to the *full* internal name, not the
  2183 bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!
  2184 
  2185 * Disposed old type and term read functions (Sign.read_def_typ,
  2186 Sign.read_typ, Sign.read_def_terms, Sign.read_term,
  2187 Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should
  2188 use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,
  2189 Syntax.read_term_global etc.; see also OldGoals.read_term as last
  2190 resort for legacy applications.
  2191 
  2192 * Disposed old declarations, tactics, tactic combinators that refer to
  2193 the simpset or claset of an implicit theory (such as Addsimps,
  2194 Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in
  2195 embedded ML text, or local_simpset_of with a proper context passed as
  2196 explicit runtime argument.
  2197 
  2198 * Rules and tactics that read instantiations (read_instantiate,
  2199 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
  2200 context, which is required for parsing and type-checking.  Moreover,
  2201 the variables are specified as plain indexnames, not string encodings
  2202 thereof.  INCOMPATIBILITY.
  2203 
  2204 * Generic Toplevel.add_hook interface allows to analyze the result of
  2205 transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
  2206 for theorem dependency output of transactions resulting in a new
  2207 theory state.
  2208 
  2209 * ML antiquotations: block-structured compilation context indicated by
  2210 \<lbrace> ... \<rbrace>; additional antiquotation forms:
  2211 
  2212   @{binding name}                         - basic name binding
  2213   @{let ?pat = term}                      - term abbreviation (HO matching)
  2214   @{note name = fact}                     - fact abbreviation
  2215   @{thm fact}                             - singleton fact (with attributes)
  2216   @{thms fact}                            - general fact (with attributes)
  2217   @{lemma prop by method}                 - singleton goal
  2218   @{lemma prop by meth1 meth2}            - singleton goal
  2219   @{lemma prop1 ... propN by method}      - general goal
  2220   @{lemma prop1 ... propN by meth1 meth2} - general goal
  2221   @{lemma (open) ...}                     - open derivation
  2222 
  2223 
  2224 *** System ***
  2225 
  2226 * The Isabelle "emacs" tool provides a specific interface to invoke
  2227 Proof General / Emacs, with more explicit failure if that is not
  2228 installed (the old isabelle-interface script silently falls back on
  2229 isabelle-process).  The PROOFGENERAL_HOME setting determines the
  2230 installation location of the Proof General distribution.
  2231 
  2232 * Isabelle/lib/classes/Pure.jar provides basic support to integrate
  2233 the Isabelle process into a JVM/Scala application.  See
  2234 Isabelle/lib/jedit/plugin for a minimal example.  (The obsolete Java
  2235 process wrapper has been discontinued.)
  2236 
  2237 * Added homegrown Isabelle font with unicode layout, see lib/fonts.
  2238 
  2239 * Various status messages (with exact source position information) are
  2240 emitted, if proper markup print mode is enabled.  This allows
  2241 user-interface components to provide detailed feedback on internal
  2242 prover operations.
  2243 
  2244 
  2245 
  2246 New in Isabelle2008 (June 2008)
  2247 -------------------------------
  2248 
  2249 *** General ***
  2250 
  2251 * The Isabelle/Isar Reference Manual (isar-ref) has been reorganized
  2252 and updated, with formally checked references as hyperlinks.
  2253 
  2254 * Theory loader: use_thy (and similar operations) no longer set the
  2255 implicit ML context, which was occasionally hard to predict and in
  2256 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
  2257 provides a proper context already.
  2258 
  2259 * Theory loader: old-style ML proof scripts being *attached* to a thy
  2260 file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
  2261 'use' within a theory file will do the job.
  2262 
  2263 * Name space merge now observes canonical order, i.e. the second space
  2264 is inserted into the first one, while existing entries in the first
  2265 space take precedence.  INCOMPATIBILITY in rare situations, may try to
  2266 swap theory imports.
  2267 
  2268 * Syntax: symbol \<chi> is now considered a letter.  Potential
  2269 INCOMPATIBILITY in identifier syntax etc.
  2270 
  2271 * Outer syntax: string tokens no longer admit escaped white space,
  2272 which was an accidental (undocumented) feature.  INCOMPATIBILITY, use
  2273 white space without escapes.
  2274 
  2275 * Outer syntax: string tokens may contain arbitrary character codes
  2276 specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
  2277 "foo_bar".
  2278 
  2279 
  2280 *** Pure ***
  2281 
  2282 * Context-dependent token translations.  Default setup reverts locally
  2283 fixed variables, and adds hilite markup for undeclared frees.
  2284 
  2285 * Unused theorems can be found using the new command 'unused_thms'.
  2286 There are three ways of invoking it:
  2287 
  2288 (1) unused_thms
  2289      Only finds unused theorems in the current theory.
  2290 
  2291 (2) unused_thms thy_1 ... thy_n -
  2292      Finds unused theorems in the current theory and all of its ancestors,
  2293      excluding the theories thy_1 ... thy_n and all of their ancestors.
  2294 
  2295 (3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m
  2296      Finds unused theorems in the theories thy'_1 ... thy'_m and all of
  2297      their ancestors, excluding the theories thy_1 ... thy_n and all of
  2298      their ancestors.
  2299 
  2300 In order to increase the readability of the list produced by
  2301 unused_thms, theorems that have been created by a particular instance
  2302 of a theory command such as 'inductive' or 'function' are considered
  2303 to belong to the same "group", meaning that if at least one theorem in
  2304 this group is used, the other theorems in the same group are no longer
  2305 reported as unused.  Moreover, if all theorems in the group are
  2306 unused, only one theorem in the group is displayed.
  2307 
  2308 Note that proof objects have to be switched on in order for
  2309 unused_thms to work properly (i.e. !proofs must be >= 1, which is
  2310 usually the case when using Proof General with the default settings).
  2311 
  2312 * Authentic naming of facts disallows ad-hoc overwriting of previous
  2313 theorems within the same name space.  INCOMPATIBILITY, need to remove
  2314 duplicate fact bindings, or even accidental fact duplications.  Note
  2315 that tools may maintain dynamically scoped facts systematically, using
  2316 PureThy.add_thms_dynamic.
  2317 
  2318 * Command 'hide' now allows to hide from "fact" name space as well.
  2319 
  2320 * Eliminated destructive theorem database, simpset, claset, and
  2321 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
  2322 update of theories within ML code.
  2323 
  2324 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
  2325 INCOMPATIBILITY, object-logics depending on former Pure require
  2326 additional setup PureThy.old_appl_syntax_setup; object-logics
  2327 depending on former CPure need to refer to Pure.
  2328 
  2329 * Commands 'use' and 'ML' are now purely functional, operating on
  2330 theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
  2331 instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
  2332 INCOMPATIBILITY.
  2333 
  2334 * Command 'setup': discontinued implicit version with ML reference.
  2335 
  2336 * Instantiation target allows for simultaneous specification of class
  2337 instance operations together with an instantiation proof.
  2338 Type-checking phase allows to refer to class operations uniformly.
  2339 See src/HOL/Complex/Complex.thy for an Isar example and
  2340 src/HOL/Library/Eval.thy for an ML example.
  2341 
  2342 * Indexing of literal facts: be more serious about including only
  2343 facts from the visible specification/proof context, but not the
  2344 background context (locale etc.).  Affects `prop` notation and method
  2345 "fact".  INCOMPATIBILITY: need to name facts explicitly in rare
  2346 situations.
  2347 
  2348 * Method "cases", "induct", "coinduct": removed obsolete/undocumented
  2349 "(open)" option, which used to expose internal bound variables to the
  2350 proof text.
  2351 
  2352 * Isar statements: removed obsolete case "rule_context".
  2353 INCOMPATIBILITY, better use explicit fixes/assumes.
  2354 
  2355 * Locale proofs: default proof step now includes 'unfold_locales';
  2356 hence 'proof' without argument may be used to unfold locale
  2357 predicates.
  2358 
  2359 
  2360 *** Document preparation ***
  2361 
  2362 * Simplified pdfsetup.sty: color/hyperref is used unconditionally for
  2363 both pdf and dvi (hyperlinks usually work in xdvi as well); removed
  2364 obsolete thumbpdf setup (contemporary PDF viewers do this on the
  2365 spot); renamed link color from "darkblue" to "linkcolor" (default
  2366 value unchanged, can be redefined via \definecolor); no longer sets
  2367 "a4paper" option (unnecessary or even intrusive).
  2368 
  2369 * Antiquotation @{lemma A method} proves proposition A by the given
  2370 method (either a method name or a method name plus (optional) method
  2371 arguments in parentheses) and prints A just like @{prop A}.
  2372 
  2373 
  2374 *** HOL ***
  2375 
  2376 * New primrec package.  Specification syntax conforms in style to
  2377 definition/function/....  No separate induction rule is provided.  The
  2378 "primrec" command distinguishes old-style and new-style specifications
  2379 by syntax.  The former primrec package is now named OldPrimrecPackage.
  2380 When adjusting theories, beware: constants stemming from new-style
  2381 primrec specifications have authentic syntax.
  2382 
  2383 * Metis prover is now an order of magnitude faster, and also works
  2384 with multithreading.
  2385 
  2386 * Metis: the maximum number of clauses that can be produced from a
  2387 theorem is now given by the attribute max_clauses.  Theorems that
  2388 exceed this number are ignored, with a warning printed.
  2389 
  2390 * Sledgehammer no longer produces structured proofs by default. To
  2391 enable, declare [[sledgehammer_full = true]].  Attributes
  2392 reconstruction_modulus, reconstruction_sorts renamed
  2393 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
  2394 
  2395 * Method "induct_scheme" derives user-specified induction rules
  2396 from well-founded induction and completeness of patterns. This factors
  2397 out some operations that are done internally by the function package
  2398 and makes them available separately.  See
  2399 src/HOL/ex/Induction_Scheme.thy for examples.
  2400 
  2401 * More flexible generation of measure functions for termination
  2402 proofs: Measure functions can be declared by proving a rule of the
  2403 form "is_measure f" and giving it the [measure_function] attribute.
  2404 The "is_measure" predicate is logically meaningless (always true), and
  2405 just guides the heuristic.  To find suitable measure functions, the
  2406 termination prover sets up the goal "is_measure ?f" of the appropriate
  2407 type and generates all solutions by prolog-style backwards proof using
  2408 the declared rules.
  2409 
  2410 This setup also deals with rules like 
  2411 
  2412   "is_measure f ==> is_measure (list_size f)"
  2413 
  2414 which accommodates nested datatypes that recurse through lists.
  2415 Similar rules are predeclared for products and option types.
  2416 
  2417 * Turned the type of sets "'a set" into an abbreviation for "'a => bool"
  2418 
  2419   INCOMPATIBILITIES:
  2420 
  2421   - Definitions of overloaded constants on sets have to be replaced by
  2422     definitions on => and bool.
  2423 
  2424   - Some definitions of overloaded operators on sets can now be proved
  2425     using the definitions of the operators on => and bool.  Therefore,
  2426     the following theorems have been renamed:
  2427 
  2428       subset_def   -> subset_eq
  2429       psubset_def  -> psubset_eq
  2430       set_diff_def -> set_diff_eq
  2431       Compl_def    -> Compl_eq
  2432       Sup_set_def  -> Sup_set_eq
  2433       Inf_set_def  -> Inf_set_eq
  2434       sup_set_def  -> sup_set_eq
  2435       inf_set_def  -> inf_set_eq
  2436 
  2437   - Due to the incompleteness of the HO unification algorithm, some
  2438     rules such as subst may require manual instantiation, if some of
  2439     the unknowns in the rule is a set.
  2440 
  2441   - Higher order unification and forward proofs:
  2442     The proof pattern
  2443 
  2444       have "P (S::'a set)" <...>
  2445       then have "EX S. P S" ..
  2446 
  2447     no longer works (due to the incompleteness of the HO unification
  2448     algorithm) and must be replaced by the pattern
  2449 
  2450       have "EX S. P S"
  2451       proof
  2452         show "P S" <...>
  2453       qed
  2454 
  2455   - Calculational reasoning with subst (or similar rules):
  2456     The proof pattern
  2457 
  2458       have "P (S::'a set)" <...>
  2459       also have "S = T" <...>
  2460       finally have "P T" .
  2461 
  2462     no longer works (for similar reasons as the previous example) and
  2463     must be replaced by something like
  2464 
  2465       have "P (S::'a set)" <...>
  2466       moreover have "S = T" <...>
  2467       ultimately have "P T" by simp
  2468 
  2469   - Tactics or packages written in ML code:
  2470     Code performing pattern matching on types via
  2471 
  2472       Type ("set", [T]) => ...
  2473 
  2474     must be rewritten. Moreover, functions like strip_type or
  2475     binder_types no longer return the right value when applied to a
  2476     type of the form
  2477 
  2478       T1 => ... => Tn => U => bool
  2479 
  2480     rather than
  2481 
  2482       T1 => ... => Tn => U set
  2483 
  2484 * Merged theories Wellfounded_Recursion, Accessible_Part and
  2485 Wellfounded_Relations to theory Wellfounded.
  2486 
  2487 * Explicit class "eq" for executable equality.  INCOMPATIBILITY.
  2488 
  2489 * Class finite no longer treats UNIV as class parameter.  Use class
  2490 enum from theory Library/Enum instead to achieve a similar effect.
  2491 INCOMPATIBILITY.
  2492 
  2493 * Theory List: rule list_induct2 now has explicitly named cases "Nil"
  2494 and "Cons".  INCOMPATIBILITY.
  2495 
  2496 * HOL (and FOL): renamed variables in rules imp_elim and swap.
  2497 Potential INCOMPATIBILITY.
  2498 
  2499 * Theory Product_Type: duplicated lemmas split_Pair_apply and
  2500 injective_fst_snd removed, use split_eta and prod_eqI instead.
  2501 Renamed upd_fst to apfst and upd_snd to apsnd.  INCOMPATIBILITY.
  2502 
  2503 * Theory Nat: removed redundant lemmas that merely duplicate lemmas of
  2504 the same name in theory Orderings:
  2505 
  2506   less_trans
  2507   less_linear
  2508   le_imp_less_or_eq
  2509   le_less_trans
  2510   less_le_trans
  2511   less_not_sym
  2512   less_asym
  2513 
  2514 Renamed less_imp_le to less_imp_le_nat, and less_irrefl to
  2515 less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types
  2516 and different variable names.
  2517 
  2518 * Library/Option_ord.thy: Canonical order on option type.
  2519 
  2520 * Library/RBT.thy: Red-black trees, an efficient implementation of
  2521 finite maps.
  2522 
  2523 * Library/Countable.thy: Type class for countable types.
  2524 
  2525 * Theory Int: The representation of numerals has changed.  The infix
  2526 operator BIT and the bit datatype with constructors B0 and B1 have
  2527 disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
  2528 place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems
  2529 involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"
  2530 accordingly.
  2531 
  2532 * Theory Nat: definition of <= and < on natural numbers no longer
  2533 depend on well-founded relations.  INCOMPATIBILITY.  Definitions
  2534 le_def and less_def have disappeared.  Consider lemmas not_less
  2535 [symmetric, where ?'a = nat] and less_eq [symmetric] instead.
  2536 
  2537 * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
  2538 (whose purpose mainly is for various fold_set functionals) have been
  2539 abandoned in favor of the existing algebraic classes
  2540 ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
  2541 lower_semilattice (resp. upper_semilattice) and linorder.
  2542 INCOMPATIBILITY.
  2543 
  2544 * Theory Transitive_Closure: induct and cases rules now declare proper
  2545 case_names ("base" and "step").  INCOMPATIBILITY.
  2546 
  2547 * Theorem Inductive.lfp_ordinal_induct generalized to complete
  2548 lattices.  The form set-specific version is available as
  2549 Inductive.lfp_ordinal_induct_set.
  2550 
  2551 * Renamed theorems "power.simps" to "power_int.simps".
  2552 INCOMPATIBILITY.
  2553 
  2554 * Class semiring_div provides basic abstract properties of semirings
  2555 with division and modulo operations.  Subsumes former class dvd_mod.
  2556 
  2557 * Merged theories IntDef, Numeral and IntArith into unified theory
  2558 Int.  INCOMPATIBILITY.
  2559 
  2560 * Theory Library/Code_Index: type "index" now represents natural
  2561 numbers rather than integers.  INCOMPATIBILITY.
  2562 
  2563 * New class "uminus" with operation "uminus" (split of from class
  2564 "minus" which now only has operation "minus", binary).
  2565 INCOMPATIBILITY.
  2566 
  2567 * Constants "card", "internal_split", "option_map" now with authentic
  2568 syntax.  INCOMPATIBILITY.
  2569 
  2570 * Definitions subset_def, psubset_def, set_diff_def, Compl_def,
  2571 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
  2572 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
  2573 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
  2574 Sup_set_def, le_def, less_def, option_map_def now with object
  2575 equality.  INCOMPATIBILITY.
  2576 
  2577 * Records. Removed K_record, and replaced it by pure lambda term
  2578 %x. c. The simplifier setup is now more robust against eta expansion.
  2579 INCOMPATIBILITY: in cases explicitly referring to K_record.
  2580 
  2581 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
  2582 
  2583 * Library/ListVector: new theory of arithmetic vector operations.
  2584 
  2585 * Library/Order_Relation: new theory of various orderings as sets of
  2586 pairs.  Defines preorders, partial orders, linear orders and
  2587 well-orders on sets and on types.
  2588 
  2589 
  2590 *** ZF ***
  2591 
  2592 * Renamed some theories to allow to loading both ZF and HOL in the
  2593 same session:
  2594 
  2595   Datatype  -> Datatype_ZF
  2596   Inductive -> Inductive_ZF
  2597   Int       -> Int_ZF
  2598   IntDiv    -> IntDiv_ZF
  2599   Nat       -> Nat_ZF
  2600   List      -> List_ZF
  2601   Main      -> Main_ZF
  2602 
  2603 INCOMPATIBILITY: ZF theories that import individual theories below
  2604 Main might need to be adapted.  Regular theory Main is still
  2605 available, as trivial extension of Main_ZF.
  2606 
  2607 
  2608 *** ML ***
  2609 
  2610 * ML within Isar: antiquotation @{const name} or @{const
  2611 name(typargs)} produces statically-checked Const term.
  2612 
  2613 * Functor NamedThmsFun: data is available to the user as dynamic fact
  2614 (of the same name).  Removed obsolete print command.
  2615 
  2616 * Removed obsolete "use_legacy_bindings" function.
  2617 
  2618 * The ``print mode'' is now a thread-local value derived from a global
  2619 template (the former print_mode reference), thus access becomes
  2620 non-critical.  The global print_mode reference is for session
  2621 management only; user-code should use print_mode_value,
  2622 print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
  2623 
  2624 * Functions system/system_out provide a robust way to invoke external
  2625 shell commands, with propagation of interrupts (requires Poly/ML
  2626 5.2.1).  Do not use OS.Process.system etc. from the basis library!
  2627 
  2628 
  2629 *** System ***
  2630 
  2631 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs ---
  2632 in accordance with Proof General 3.7, which prefers GNU emacs.
  2633 
  2634 * isatool tty runs Isabelle process with plain tty interaction;
  2635 optional line editor may be specified via ISABELLE_LINE_EDITOR
  2636 setting, the default settings attempt to locate "ledit" and "rlwrap".
  2637 
  2638 * isatool browser now works with Cygwin as well, using general
  2639 "javapath" function defined in Isabelle process environment.
  2640 
  2641 * YXML notation provides a simple and efficient alternative to
  2642 standard XML transfer syntax.  See src/Pure/General/yxml.ML and
  2643 isatool yxml as described in the Isabelle system manual.
  2644 
  2645 * JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes)
  2646 provides general wrapper for managing an Isabelle process in a robust
  2647 fashion, with ``cooked'' output from stdin/stderr.
  2648 
  2649 * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit),
  2650 based on Isabelle/JVM process wrapper (see Isabelle/lib/classes).
  2651 
  2652 * Removed obsolete THIS_IS_ISABELLE_BUILD feature.  NB: the documented
  2653 way of changing the user's settings is via
  2654 ISABELLE_HOME_USER/etc/settings, which is a fully featured bash
  2655 script.
  2656 
  2657 * Multithreading.max_threads := 0 refers to the number of actual CPU
  2658 cores of the underlying machine, which is a good starting point for
  2659 optimal performance tuning.  The corresponding usedir option -M allows
  2660 "max" as an alias for "0".  WARNING: does not work on certain versions
  2661 of Mac OS (with Poly/ML 5.1).
  2662 
  2663 * isabelle-process: non-ML sessions are run with "nice", to reduce the
  2664 adverse effect of Isabelle flooding interactive front-ends (notably
  2665 ProofGeneral / XEmacs).
  2666 
  2667 
  2668 
  2669 New in Isabelle2007 (November 2007)
  2670 -----------------------------------
  2671 
  2672 *** General ***
  2673 
  2674 * More uniform information about legacy features, notably a
  2675 warning/error of "Legacy feature: ...", depending on the state of the
  2676 tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY:
  2677 legacy features will disappear eventually.
  2678 
  2679 * Theory syntax: the header format ``theory A = B + C:'' has been
  2680 discontinued in favour of ``theory A imports B C begin''.  Use isatool
  2681 fixheaders to convert existing theory files.  INCOMPATIBILITY.
  2682 
  2683 * Theory syntax: the old non-Isar theory file format has been
  2684 discontinued altogether.  Note that ML proof scripts may still be used
  2685 with Isar theories; migration is usually quite simple with the ML
  2686 function use_legacy_bindings.  INCOMPATIBILITY.
  2687 
  2688 * Theory syntax: some popular names (e.g. 'class', 'declaration',
  2689 'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double
  2690 quotes.
  2691 
  2692 * Theory loader: be more serious about observing the static theory
  2693 header specifications (including optional directories), but not the
  2694 accidental file locations of previously successful loads.  The strict
  2695 update policy of former update_thy is now already performed by
  2696 use_thy, so the former has been removed; use_thys updates several
  2697 theories simultaneously, just as 'imports' within a theory header
  2698 specification, but without merging the results.  Potential
  2699 INCOMPATIBILITY: may need to refine theory headers and commands
  2700 ROOT.ML which depend on load order.
  2701 
  2702 * Theory loader: optional support for content-based file
  2703 identification, instead of the traditional scheme of full physical
  2704 path plus date stamp; configured by the ISABELLE_FILE_IDENT setting
  2705 (cf. the system manual).  The new scheme allows to work with
  2706 non-finished theories in persistent session images, such that source
  2707 files may be moved later on without requiring reloads.
  2708 
  2709 * Theory loader: old-style ML proof scripts being *attached* to a thy
  2710 file (with the same base name as the theory) are considered a legacy
  2711 feature, which will disappear eventually. Even now, the theory loader
  2712 no longer maintains dependencies on such files.
  2713 
  2714 * Syntax: the scope for resolving ambiguities via type-inference is
  2715 now limited to individual terms, instead of whole simultaneous
  2716 specifications as before. This greatly reduces the complexity of the
  2717 syntax module and improves flexibility by separating parsing and
  2718 type-checking. INCOMPATIBILITY: additional type-constraints (explicit
  2719 'fixes' etc.) are required in rare situations.
  2720 
  2721 * Syntax: constants introduced by new-style packages ('definition',
  2722 'abbreviation' etc.) are passed through the syntax module in
  2723 ``authentic mode''. This means that associated mixfix annotations
  2724 really stick to such constants, independently of potential name space
  2725 ambiguities introduced later on. INCOMPATIBILITY: constants in parse
  2726 trees are represented slightly differently, may need to adapt syntax
  2727 translations accordingly. Use CONST marker in 'translations' and
  2728 @{const_syntax} antiquotation in 'parse_translation' etc.
  2729 
  2730 * Legacy goal package: reduced interface to the bare minimum required
  2731 to keep existing proof scripts running.  Most other user-level
  2732 functions are now part of the OldGoals structure, which is *not* open
  2733 by default (consider isatool expandshort before open OldGoals).
  2734 Removed top_sg, prin, printyp, pprint_term/typ altogether, because
  2735 these tend to cause confusion about the actual goal (!) context being
  2736 used here, which is not necessarily the same as the_context().
  2737 
  2738 * Command 'find_theorems': supports "*" wild-card in "name:"
  2739 criterion; "with_dups" option.  Certain ProofGeneral versions might
  2740 support a specific search form (see ProofGeneral/CHANGES).
  2741 
  2742 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
  2743 by default, which means that "prems" (and also "fixed variables") are
  2744 suppressed from proof state output.  Note that the ProofGeneral
  2745 settings mechanism allows to change and save options persistently, but
  2746 older versions of Isabelle will fail to start up if a negative prems
  2747 limit is imposed.
  2748 
  2749 * Local theory targets may be specified by non-nested blocks of
  2750 ``context/locale/class ... begin'' followed by ``end''.  The body may
  2751 contain definitions, theorems etc., including any derived mechanism
  2752 that has been implemented on top of these primitives.  This concept
  2753 generalizes the existing ``theorem (in ...)'' towards more versatility
  2754 and scalability.
  2755 
  2756 * Proof General interface: proper undo of final 'end' command;
  2757 discontinued Isabelle/classic mode (ML proof scripts).
  2758 
  2759 
  2760 *** Document preparation ***
  2761 
  2762 * Added antiquotation @{theory name} which prints the given name,
  2763 after checking that it refers to a valid ancestor theory in the
  2764 current context.
  2765 
  2766 * Added antiquotations @{ML_type text} and @{ML_struct text} which
  2767 check the given source text as ML type/structure, printing verbatim.
  2768 
  2769 * Added antiquotation @{abbrev "c args"} which prints the abbreviation
  2770 "c args == rhs" given in the current context.  (Any number of
  2771 arguments may be given on the LHS.)
  2772 
  2773 
  2774 *** Pure ***
  2775 
  2776 * The 'class' package offers a combination of axclass and locale to
  2777 achieve Haskell-like type classes in Isabelle.  Definitions and
  2778 theorems within a class context produce both relative results (with
  2779 implicit parameters according to the locale context), and polymorphic
  2780 constants with qualified polymorphism (according to the class
  2781 context).  Within the body context of a 'class' target, a separate
  2782 syntax layer ("user space type system") takes care of converting
  2783 between global polymorphic consts and internal locale representation.
  2784 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).
  2785 "isatool doc classes" provides a tutorial.
  2786 
  2787 * Generic code generator framework allows to generate executable
  2788 code for ML and Haskell (including Isabelle classes).  A short usage
  2789 sketch:
  2790 
  2791     internal compilation:
  2792         export_code <list of constants (term syntax)> in SML
  2793     writing SML code to a file:
  2794         export_code <list of constants (term syntax)> in SML <filename>
  2795     writing OCaml code to a file:
  2796         export_code <list of constants (term syntax)> in OCaml <filename>
  2797     writing Haskell code to a bunch of files:
  2798         export_code <list of constants (term syntax)> in Haskell <filename>
  2799 
  2800     evaluating closed propositions to True/False using code generation:
  2801         method ``eval''
  2802 
  2803 Reasonable default setup of framework in HOL.
  2804 
  2805 Theorem attributs for selecting and transforming function equations theorems:
  2806 
  2807     [code fun]:        select a theorem as function equation for a specific constant
  2808     [code fun del]:    deselect a theorem as function equation for a specific constant
  2809     [code inline]:     select an equation theorem for unfolding (inlining) in place
  2810     [code inline del]: deselect an equation theorem for unfolding (inlining) in place
  2811 
  2812 User-defined serializations (target in {SML, OCaml, Haskell}):
  2813 
  2814     code_const <and-list of constants (term syntax)>
  2815       {(target) <and-list of const target syntax>}+
  2816 
  2817     code_type <and-list of type constructors>
  2818       {(target) <and-list of type target syntax>}+
  2819 
  2820     code_instance <and-list of instances>
  2821       {(target)}+
  2822         where instance ::= <type constructor> :: <class>
  2823 
  2824     code_class <and_list of classes>
  2825       {(target) <and-list of class target syntax>}+
  2826         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
  2827 
  2828 code_instance and code_class only are effective to target Haskell.
  2829 
  2830 For example usage see src/HOL/ex/Codegenerator.thy and
  2831 src/HOL/ex/Codegenerator_Pretty.thy.  A separate tutorial on code
  2832 generation from Isabelle/HOL theories is available via "isatool doc
  2833 codegen".
  2834 
  2835 * Code generator: consts in 'consts_code' Isar commands are now
  2836 referred to by usual term syntax (including optional type
  2837 annotations).
  2838 
  2839 * Command 'no_translations' removes translation rules from theory
  2840 syntax.
  2841 
  2842 * Overloaded definitions are now actually checked for acyclic
  2843 dependencies.  The overloading scheme is slightly more general than
  2844 that of Haskell98, although Isabelle does not demand an exact
  2845 correspondence to type class and instance declarations.
  2846 INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more
  2847 exotic versions of overloading -- at the discretion of the user!
  2848 
  2849 Polymorphic constants are represented via type arguments, i.e. the
  2850 instantiation that matches an instance against the most general
  2851 declaration given in the signature.  For example, with the declaration
  2852 c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented
  2853 as c(nat).  Overloading is essentially simultaneous structural
  2854 recursion over such type arguments.  Incomplete specification patterns
  2855 impose global constraints on all occurrences, e.g. c('a * 'a) on the
  2856 LHS means that more general c('a * 'b) will be disallowed on any RHS.
  2857 Command 'print_theory' outputs the normalized system of recursive
  2858 equations, see section "definitions".
  2859 
  2860 * Configuration options are maintained within the theory or proof
  2861 context (with name and type bool/int/string), providing a very simple
  2862 interface to a poor-man's version of general context data.  Tools may
  2863 declare options in ML (e.g. using Attrib.config_int) and then refer to
  2864 these values using Config.get etc.  Users may change options via an
  2865 associated attribute of the same name.  This form of context
  2866 declaration works particularly well with commands 'declare' or
  2867 'using', for example ``declare [[foo = 42]]''.  Thus it has become
  2868 very easy to avoid global references, which would not observe Isar
  2869 toplevel undo/redo and fail to work with multithreading.
  2870 
  2871 Various global ML references of Pure and HOL have been turned into
  2872 configuration options:
  2873 
  2874   Unify.search_bound		unify_search_bound
  2875   Unify.trace_bound		unify_trace_bound
  2876   Unify.trace_simp		unify_trace_simp
  2877   Unify.trace_types		unify_trace_types
  2878   Simplifier.simp_depth_limit	simp_depth_limit
  2879   Blast.depth_limit		blast_depth_limit
  2880   DatatypeProp.dtK		datatype_distinctness_limit
  2881   fast_arith_neq_limit  	fast_arith_neq_limit
  2882   fast_arith_split_limit	fast_arith_split_limit
  2883 
  2884 * Named collections of theorems may be easily installed as context
  2885 data using the functor NamedThmsFun (see also
  2886 src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
  2887 attributes; there is also a toplevel print command.  This facility is
  2888 just a common case of general context data, which is the preferred way
  2889 for anything more complex than just a list of facts in canonical
  2890 order.
  2891 
  2892 * Isar: command 'declaration' augments a local theory by generic
  2893 declaration functions written in ML.  This enables arbitrary content
  2894 being added to the context, depending on a morphism that tells the
  2895 difference of the original declaration context wrt. the application
  2896 context encountered later on.
  2897 
  2898 * Isar: proper interfaces for simplification procedures.  Command
  2899 'simproc_setup' declares named simprocs (with match patterns, and body
  2900 text in ML).  Attribute "simproc" adds/deletes simprocs in the current
  2901 context.  ML antiquotation @{simproc name} retrieves named simprocs.
  2902 
  2903 * Isar: an extra pair of brackets around attribute declarations
  2904 abbreviates a theorem reference involving an internal dummy fact,
  2905 which will be ignored later --- only the effect of the attribute on
  2906 the background context will persist.  This form of in-place
  2907 declarations is particularly useful with commands like 'declare' and
  2908 'using', for example ``have A using [[simproc a]] by simp''.
  2909 
  2910 * Isar: method "assumption" (and implicit closing of subproofs) now
  2911 takes simple non-atomic goal assumptions into account: after applying
  2912 an assumption as a rule the resulting subgoals are solved by atomic
  2913 assumption steps.  This is particularly useful to finish 'obtain'
  2914 goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",
  2915 without referring to the original premise "!!x. P x ==> thesis" in the
  2916 Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is
  2917 more permissive.
  2918 
  2919 * Isar: implicit use of prems from the Isar proof context is
  2920 considered a legacy feature.  Common applications like ``have A .''
  2921 may be replaced by ``have A by fact'' or ``note `A`''.  In general,
  2922 referencing facts explicitly here improves readability and
  2923 maintainability of proof texts.
  2924 
  2925 * Isar: improper proof element 'guess' is like 'obtain', but derives
  2926 the obtained context from the course of reasoning!  For example:
  2927 
  2928   assume "EX x y. A x & B y"   -- "any previous fact"
  2929   then guess x and y by clarify
  2930 
  2931 This technique is potentially adventurous, depending on the facts and
  2932 proof tools being involved here.
  2933 
  2934 * Isar: known facts from the proof context may be specified as literal
  2935 propositions, using ASCII back-quote syntax.  This works wherever
  2936 named facts used to be allowed so far, in proof commands, proof
  2937 methods, attributes etc.  Literal facts are retrieved from the context
  2938 according to unification of type and term parameters.  For example,
  2939 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
  2940 theorems in the current context, then these are valid literal facts:
  2941 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
  2942 
  2943 There is also a proof method "fact" which does the same composition
  2944 for explicit goal states, e.g. the following proof texts coincide with
  2945 certain special cases of literal facts:
  2946 
  2947   have "A" by fact                 ==  note `A`
  2948   have "A ==> B" by fact           ==  note `A ==> B`
  2949   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
  2950   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
  2951 
  2952 * Isar: ":" (colon) is no longer a symbolic identifier character in
  2953 outer syntax.  Thus symbolic identifiers may be used without
  2954 additional white space in declarations like this: ``assume *: A''.
  2955 
  2956 * Isar: 'print_facts' prints all local facts of the current context,
  2957 both named and unnamed ones.
  2958 
  2959 * Isar: 'def' now admits simultaneous definitions, e.g.:
  2960 
  2961   def x == "t" and y == "u"
  2962 
  2963 * Isar: added command 'unfolding', which is structurally similar to
  2964 'using', but affects both the goal state and facts by unfolding given
  2965 rewrite rules.  Thus many occurrences of the 'unfold' method or
  2966 'unfolded' attribute may be replaced by first-class proof text.
  2967 
  2968 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded',
  2969 and command 'unfolding' now all support object-level equalities
  2970 (potentially conditional).  The underlying notion of rewrite rule is
  2971 analogous to the 'rule_format' attribute, but *not* that of the
  2972 Simplifier (which is usually more generous).
  2973 
  2974 * Isar: the new attribute [rotated n] (default n = 1) rotates the
  2975 premises of a theorem by n. Useful in conjunction with drule.
  2976 
  2977 * Isar: the goal restriction operator [N] (default N = 1) evaluates a
  2978 method expression within a sandbox consisting of the first N
  2979 sub-goals, which need to exist.  For example, ``simp_all [3]''
  2980 simplifies the first three sub-goals, while (rule foo, simp_all)[]
  2981 simplifies all new goals that emerge from applying rule foo to the
  2982 originally first one.
  2983 
  2984 * Isar: schematic goals are no longer restricted to higher-order
  2985 patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as
  2986 expected.
  2987 
  2988 * Isar: the conclusion of a long theorem statement is now either
  2989 'shows' (a simultaneous conjunction, as before), or 'obtains'
  2990 (essentially a disjunction of cases with local parameters and
  2991 assumptions).  The latter allows to express general elimination rules
  2992 adequately; in this notation common elimination rules look like this:
  2993 
  2994   lemma exE:    -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis"
  2995     assumes "EX x. P x"
  2996     obtains x where "P x"
  2997 
  2998   lemma conjE:  -- "A & B ==> (A ==> B ==> thesis) ==> thesis"
  2999     assumes "A & B"
  3000     obtains A and B
  3001 
  3002   lemma disjE:  -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis"
  3003     assumes "A | B"
  3004     obtains
  3005       A
  3006     | B
  3007 
  3008 The subsequent classical rules even refer to the formal "thesis"
  3009 explicitly:
  3010 
  3011   lemma classical:     -- "(~ thesis ==> thesis) ==> thesis"
  3012     obtains "~ thesis"
  3013 
  3014   lemma Peirce's_Law:  -- "((thesis ==> something) ==> thesis) ==> thesis"
  3015     obtains "thesis ==> something"
  3016 
  3017 The actual proof of an 'obtains' statement is analogous to that of the
  3018 Isar proof element 'obtain', only that there may be several cases.
  3019 Optional case names may be specified in parentheses; these will be
  3020 available both in the present proof and as annotations in the
  3021 resulting rule, for later use with the 'cases' method (cf. attribute
  3022 case_names).
  3023 
  3024 * Isar: the assumptions of a long theorem statement are available as
  3025 "assms" fact in the proof context.  This is more appropriate than the
  3026 (historical) "prems", which refers to all assumptions of the current
  3027 context, including those from the target locale, proof body etc.
  3028 
  3029 * Isar: 'print_statement' prints theorems from the current theory or
  3030 proof context in long statement form, according to the syntax of a
  3031 top-level lemma.
  3032 
  3033 * Isar: 'obtain' takes an optional case name for the local context
  3034 introduction rule (default "that").
  3035 
  3036 * Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use
  3037 explicit (is "_ ==> ?foo") in the rare cases where this still happens
  3038 to occur.
  3039 
  3040 * Pure: syntax "CONST name" produces a fully internalized constant
  3041 according to the current context.  This is particularly useful for
  3042 syntax translations that should refer to internal constant
  3043 representations independently of name spaces.
  3044 
  3045 * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"
  3046 instead of "FOO ". This allows multiple binder declarations to coexist
  3047 in the same context.  INCOMPATIBILITY.
  3048 
  3049 * Isar/locales: 'notation' provides a robust interface to the 'syntax'
  3050 primitive that also works in a locale context (both for constants and
  3051 fixed variables). Type declaration and internal syntactic representation
  3052 of given constants retrieved from the context. Likewise, the
  3053 'no_notation' command allows to remove given syntax annotations from the
  3054 current context.
  3055 
  3056 * Isar/locales: new derived specification elements 'axiomatization',
  3057 'definition', 'abbreviation', which support type-inference, admit
  3058 object-level specifications (equality, equivalence).  See also the
  3059 isar-ref manual.  Examples:
  3060 
  3061   axiomatization
  3062     eq  (infix "===" 50) where
  3063     eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
  3064 
  3065   definition "f x y = x + y + 1"
  3066   definition g where "g x = f x x"
  3067 
  3068   abbreviation
  3069     neq  (infix "=!=" 50) where
  3070     "x =!= y == ~ (x === y)"
  3071 
  3072 These specifications may be also used in a locale context.  Then the
  3073 constants being introduced depend on certain fixed parameters, and the
  3074 constant name is qualified by the locale base name.  An internal
  3075 abbreviation takes care for convenient input and output, making the
  3076 parameters implicit and using the original short name.  See also
  3077 src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
  3078 entities from a monomorphic theory.
  3079 
  3080 Presently, abbreviations are only available 'in' a target locale, but
  3081 not inherited by general import expressions.  Also note that
  3082 'abbreviation' may be used as a type-safe replacement for 'syntax' +
  3083 'translations' in common applications.  The "no_abbrevs" print mode
  3084 prevents folding of abbreviations in term output.
  3085 
  3086 Concrete syntax is attached to specified constants in internal form,
  3087 independently of name spaces.  The parse tree representation is
  3088 slightly different -- use 'notation' instead of raw 'syntax', and
  3089 'translations' with explicit "CONST" markup to accommodate this.
  3090 
  3091 * Pure/Isar: unified syntax for new-style specification mechanisms
  3092 (e.g.  'definition', 'abbreviation', or 'inductive' in HOL) admits
  3093 full type inference and dummy patterns ("_").  For example:
  3094 
  3095   definition "K x _ = x"
  3096 
  3097   inductive conj for A B
  3098   where "A ==> B ==> conj A B"
  3099 
  3100 * Pure: command 'print_abbrevs' prints all constant abbreviations of
  3101 the current context.  Print mode "no_abbrevs" prevents inversion of
  3102 abbreviations on output.
  3103 
  3104 * Isar/locales: improved parameter handling: use of locales "var" and
  3105 "struct" no longer necessary; - parameter renamings are no longer
  3106 required to be injective.  For example, this allows to define
  3107 endomorphisms as locale endom = homom mult mult h.
  3108 
  3109 * Isar/locales: changed the way locales with predicates are defined.
  3110 Instead of accumulating the specification, the imported expression is
  3111 now an interpretation.  INCOMPATIBILITY: different normal form of
  3112 locale expressions.  In particular, in interpretations of locales with
  3113 predicates, goals repesenting already interpreted fragments are not
  3114 removed automatically.  Use methods `intro_locales' and
  3115 `unfold_locales'; see below.
  3116 
  3117 * Isar/locales: new methods `intro_locales' and `unfold_locales'
  3118 provide backward reasoning on locales predicates.  The methods are
  3119 aware of interpretations and discharge corresponding goals.
  3120 `intro_locales' is less aggressive then `unfold_locales' and does not
  3121 unfold predicates to assumptions.
  3122 
  3123 * Isar/locales: the order in which locale fragments are accumulated
  3124 has changed.  This enables to override declarations from fragments due
  3125 to interpretations -- for example, unwanted simp rules.
  3126 
  3127 * Isar/locales: interpretation in theories and proof contexts has been
  3128 extended.  One may now specify (and prove) equations, which are
  3129 unfolded in interpreted theorems.  This is useful for replacing
  3130 defined concepts (constants depending on locale parameters) by
  3131 concepts already existing in the target context.  Example:
  3132 
  3133   interpretation partial_order ["op <= :: [int, int] => bool"]
  3134     where "partial_order.less (op <=) (x::int) y = (x < y)"
  3135 
  3136 Typically, the constant `partial_order.less' is created by a
  3137 definition specification element in the context of locale
  3138 partial_order.
  3139 
  3140 * Method "induct": improved internal context management to support
  3141 local fixes and defines on-the-fly. Thus explicit meta-level
  3142 connectives !!  and ==> are rarely required anymore in inductive goals
  3143 (using object-logic connectives for this purpose has been long
  3144 obsolete anyway). Common proof patterns are explained in
  3145 src/HOL/Induct/Common_Patterns.thy, see also
  3146 src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic
  3147 examples.
  3148 
  3149 * Method "induct": improved handling of simultaneous goals. Instead of
  3150 introducing object-level conjunction, the statement is now split into
  3151 several conclusions, while the corresponding symbolic cases are nested
  3152 accordingly. INCOMPATIBILITY, proofs need to be structured explicitly,
  3153 see src/HOL/Induct/Common_Patterns.thy, for example.
  3154 
  3155 * Method "induct": mutual induction rules are now specified as a list
  3156 of rule sharing the same induction cases. HOL packages usually provide
  3157 foo_bar.inducts for mutually defined items foo and bar (e.g. inductive
  3158 predicates/sets or datatypes). INCOMPATIBILITY, users need to specify
  3159 mutual induction rules differently, i.e. like this:
  3160 
  3161   (induct rule: foo_bar.inducts)
  3162   (induct set: foo bar)
  3163   (induct pred: foo bar)
  3164   (induct type: foo bar)
  3165 
  3166 The ML function ProjectRule.projections turns old-style rules into the
  3167 new format.
  3168 
  3169 * Method "coinduct": dual of induction, see
  3170 src/HOL/Library/Coinductive_List.thy for various examples.
  3171 
  3172 * Method "cases", "induct", "coinduct": the ``(open)'' option is
  3173 considered a legacy feature.
  3174 
  3175 * Attribute "symmetric" produces result with standardized schematic
  3176 variables (index 0).  Potential INCOMPATIBILITY.
  3177 
  3178 * Simplifier: by default the simplifier trace only shows top level
  3179 rewrites now. That is, trace_simp_depth_limit is set to 1 by
  3180 default. Thus there is less danger of being flooded by the trace. The
  3181 trace indicates where parts have been suppressed.
  3182   
  3183 * Provers/classical: removed obsolete classical version of elim_format
  3184 attribute; classical elim/dest rules are now treated uniformly when
  3185 manipulating the claset.
  3186 
  3187 * Provers/classical: stricter checks to ensure that supplied intro,
  3188 dest and elim rules are well-formed; dest and elim rules must have at
  3189 least one premise.
  3190 
  3191 * Provers/classical: attributes dest/elim/intro take an optional
  3192 weight argument for the rule (just as the Pure versions).  Weights are
  3193 ignored by automated tools, but determine the search order of single
  3194 rule steps.
  3195 
  3196 * Syntax: input syntax now supports dummy variable binding "%_. b",
  3197 where the body does not mention the bound variable.  Note that dummy
  3198 patterns implicitly depend on their context of bounds, which makes
  3199 "{_. _}" match any set comprehension as expected.  Potential
  3200 INCOMPATIBILITY -- parse translations need to cope with syntactic
  3201 constant "_idtdummy" in the binding position.
  3202 
  3203 * Syntax: removed obsolete syntactic constant "_K" and its associated
  3204 parse translation.  INCOMPATIBILITY -- use dummy abstraction instead,
  3205 for example "A -> B" => "Pi A (%_. B)".
  3206 
  3207 * Pure: 'class_deps' command visualizes the subclass relation, using
  3208 the graph browser tool.
  3209 
  3210 * Pure: 'print_theory' now suppresses certain internal declarations by
  3211 default; use '!' option for full details.
  3212 
  3213 
  3214 *** HOL ***
  3215 
  3216 * Method "metis" proves goals by applying the Metis general-purpose
  3217 resolution prover (see also http://gilith.com/software/metis/).
  3218 Examples are in the directory MetisExamples.  WARNING: the
  3219 Isabelle/HOL-Metis integration does not yet work properly with
  3220 multi-threading.
  3221   
  3222 * Command 'sledgehammer' invokes external automatic theorem provers as
  3223 background processes.  It generates calls to the "metis" method if
  3224 successful. These can be pasted into the proof.  Users do not have to
  3225 wait for the automatic provers to return.  WARNING: does not really
  3226 work with multi-threading.
  3227 
  3228 * New "auto_quickcheck" feature tests outermost goal statements for
  3229 potential counter-examples.  Controlled by ML references
  3230 auto_quickcheck (default true) and auto_quickcheck_time_limit (default
  3231 5000 milliseconds).  Fails silently if statements is outside of
  3232 executable fragment, or any other codgenerator problem occurs.
  3233 
  3234 * New constant "undefined" with axiom "undefined x = undefined".
  3235 
  3236 * Added class "HOL.eq", allowing for code generation with polymorphic
  3237 equality.
  3238 
  3239 * Some renaming of class constants due to canonical name prefixing in
  3240 the new 'class' package:
  3241 
  3242     HOL.abs ~> HOL.abs_class.abs
  3243     HOL.divide ~> HOL.divide_class.divide
  3244     0 ~> HOL.zero_class.zero
  3245     1 ~> HOL.one_class.one
  3246     op + ~> HOL.plus_class.plus
  3247     op - ~> HOL.minus_class.minus
  3248     uminus ~> HOL.minus_class.uminus
  3249     op * ~> HOL.times_class.times
  3250     op < ~> HOL.ord_class.less
  3251     op <= > HOL.ord_class.less_eq
  3252     Nat.power ~> Power.power_class.power
  3253     Nat.size ~> Nat.size_class.size
  3254     Numeral.number_of ~> Numeral.number_class.number_of
  3255     FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf
  3256     FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup
  3257     Orderings.min ~> Orderings.ord_class.min
  3258     Orderings.max ~> Orderings.ord_class.max
  3259     Divides.op div ~> Divides.div_class.div
  3260     Divides.op mod ~> Divides.div_class.mod
  3261     Divides.op dvd ~> Divides.div_class.dvd
  3262 
  3263 INCOMPATIBILITY.  Adaptions may be required in the following cases:
  3264 
  3265 a) User-defined constants using any of the names "plus", "minus",
  3266 "times", "less" or "less_eq". The standard syntax translations for
  3267 "+", "-" and "*" may go wrong.  INCOMPATIBILITY: use more specific
  3268 names.
  3269 
  3270 b) Variables named "plus", "minus", "times", "less", "less_eq"
  3271 INCOMPATIBILITY: use more specific names.
  3272 
  3273 c) Permutative equations (e.g. "a + b = b + a")
  3274 Since the change of names also changes the order of terms, permutative
  3275 rewrite rules may get applied in a different order. Experience shows
  3276 that this is rarely the case (only two adaptions in the whole Isabelle
  3277 distribution).  INCOMPATIBILITY: rewrite proofs
  3278 
  3279 d) ML code directly refering to constant names
  3280 This in general only affects hand-written proof tactics, simprocs and
  3281 so on.  INCOMPATIBILITY: grep your sourcecode and replace names.
  3282 Consider using @{const_name} antiquotation.
  3283 
  3284 * New class "default" with associated constant "default".
  3285 
  3286 * Function "sgn" is now overloaded and available on int, real, complex
  3287 (and other numeric types), using class "sgn".  Two possible defs of
  3288 sgn are given as equational assumptions in the classes sgn_if and
  3289 sgn_div_norm; ordered_idom now also inherits from sgn_if.
  3290 INCOMPATIBILITY.
  3291 
  3292 * Locale "partial_order" now unified with class "order" (cf. theory
  3293 Orderings), added parameter "less".  INCOMPATIBILITY.
  3294 
  3295 * Renamings in classes "order" and "linorder": facts "refl", "trans" and
  3296 "cases" to "order_refl", "order_trans" and "linorder_cases", to avoid
  3297 clashes with HOL "refl" and "trans".  INCOMPATIBILITY.
  3298 
  3299 * Classes "order" and "linorder": potential INCOMPATIBILITY due to
  3300 changed order of proof goals in instance proofs.
  3301 
  3302 * The transitivity reasoner for partial and linear orders is set up
  3303 for classes "order" and "linorder".  Instances of the reasoner are available
  3304 in all contexts importing or interpreting the corresponding locales.
  3305 Method "order" invokes the reasoner separately; the reasoner
  3306 is also integrated with the Simplifier as a solver.  Diagnostic
  3307 command 'print_orders' shows the available instances of the reasoner
  3308 in the current context.
  3309 
  3310 * Localized monotonicity predicate in theory "Orderings"; integrated
  3311 lemmas max_of_mono and min_of_mono with this predicate.
  3312 INCOMPATIBILITY.
  3313 
  3314 * Formulation of theorem "dense" changed slightly due to integration
  3315 with new class dense_linear_order.
  3316 
  3317 * Uniform lattice theory development in HOL.
  3318 
  3319     constants "meet" and "join" now named "inf" and "sup"
  3320     constant "Meet" now named "Inf"
  3321 
  3322     classes "meet_semilorder" and "join_semilorder" now named
  3323       "lower_semilattice" and "upper_semilattice"
  3324     class "lorder" now named "lattice"
  3325     class "comp_lat" now named "complete_lattice"
  3326 
  3327     Instantiation of lattice classes allows explicit definitions
  3328     for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices).
  3329 
  3330   INCOMPATIBILITY.  Theorem renames:
  3331 
  3332     meet_left_le            ~> inf_le1
  3333     meet_right_le           ~> inf_le2
  3334     join_left_le            ~> sup_ge1
  3335     join_right_le           ~> sup_ge2
  3336     meet_join_le            ~> inf_sup_ord
  3337     le_meetI                ~> le_infI
  3338     join_leI                ~> le_supI
  3339     le_meet                 ~> le_inf_iff
  3340     le_join                 ~> ge_sup_conv
  3341     meet_idempotent         ~> inf_idem
  3342     join_idempotent         ~> sup_idem
  3343     meet_comm               ~> inf_commute
  3344     join_comm               ~> sup_commute
  3345     meet_leI1               ~> le_infI1
  3346     meet_leI2               ~> le_infI2
  3347     le_joinI1               ~> le_supI1
  3348     le_joinI2               ~> le_supI2
  3349     meet_assoc              ~> inf_assoc
  3350     join_assoc              ~> sup_assoc
  3351     meet_left_comm          ~> inf_left_commute
  3352     meet_left_idempotent    ~> inf_left_idem
  3353     join_left_comm          ~> sup_left_commute
  3354     join_left_idempotent    ~> sup_left_idem
  3355     meet_aci                ~> inf_aci
  3356     join_aci                ~> sup_aci
  3357     le_def_meet             ~> le_iff_inf
  3358     le_def_join             ~> le_iff_sup
  3359     join_absorp2            ~> sup_absorb2
  3360     join_absorp1            ~> sup_absorb1
  3361     meet_absorp1            ~> inf_absorb1
  3362     meet_absorp2            ~> inf_absorb2
  3363     meet_join_absorp        ~> inf_sup_absorb
  3364     join_meet_absorp        ~> sup_inf_absorb
  3365     distrib_join_le         ~> distrib_sup_le
  3366     distrib_meet_le         ~> distrib_inf_le
  3367 
  3368     add_meet_distrib_left   ~> add_inf_distrib_left
  3369     add_join_distrib_left   ~> add_sup_distrib_left
  3370     is_join_neg_meet        ~> is_join_neg_inf
  3371     is_meet_neg_join        ~> is_meet_neg_sup
  3372     add_meet_distrib_right  ~> add_inf_distrib_right
  3373     add_join_distrib_right  ~> add_sup_distrib_right
  3374     add_meet_join_distribs  ~> add_sup_inf_distribs
  3375     join_eq_neg_meet        ~> sup_eq_neg_inf
  3376     meet_eq_neg_join        ~> inf_eq_neg_sup
  3377     add_eq_meet_join        ~> add_eq_inf_sup
  3378     meet_0_imp_0            ~> inf_0_imp_0
  3379     join_0_imp_0            ~> sup_0_imp_0
  3380     meet_0_eq_0             ~> inf_0_eq_0
  3381     join_0_eq_0             ~> sup_0_eq_0
  3382     neg_meet_eq_join        ~> neg_inf_eq_sup
  3383     neg_join_eq_meet        ~> neg_sup_eq_inf
  3384     join_eq_if              ~> sup_eq_if
  3385 
  3386     mono_meet               ~> mono_inf
  3387     mono_join               ~> mono_sup
  3388     meet_bool_eq            ~> inf_bool_eq
  3389     join_bool_eq            ~> sup_bool_eq
  3390     meet_fun_eq             ~> inf_fun_eq
  3391     join_fun_eq             ~> sup_fun_eq
  3392     meet_set_eq             ~> inf_set_eq
  3393     join_set_eq             ~> sup_set_eq
  3394     meet1_iff               ~> inf1_iff
  3395     meet2_iff               ~> inf2_iff
  3396     meet1I                  ~> inf1I
  3397     meet2I                  ~> inf2I
  3398     meet1D1                 ~> inf1D1
  3399     meet2D1                 ~> inf2D1
  3400     meet1D2                 ~> inf1D2
  3401     meet2D2                 ~> inf2D2
  3402     meet1E                  ~> inf1E
  3403     meet2E                  ~> inf2E
  3404     join1_iff               ~> sup1_iff
  3405     join2_iff               ~> sup2_iff
  3406     join1I1                 ~> sup1I1
  3407     join2I1                 ~> sup2I1
  3408     join1I1                 ~> sup1I1
  3409     join2I2                 ~> sup1I2
  3410     join1CI                 ~> sup1CI
  3411     join2CI                 ~> sup2CI
  3412     join1E                  ~> sup1E
  3413     join2E                  ~> sup2E
  3414 
  3415     is_meet_Meet            ~> is_meet_Inf
  3416     Meet_bool_def           ~> Inf_bool_def
  3417     Meet_fun_def            ~> Inf_fun_def
  3418     Meet_greatest           ~> Inf_greatest
  3419     Meet_lower              ~> Inf_lower
  3420     Meet_set_def            ~> Inf_set_def
  3421 
  3422     Sup_def                 ~> Sup_Inf
  3423     Sup_bool_eq             ~> Sup_bool_def
  3424     Sup_fun_eq              ~> Sup_fun_def
  3425     Sup_set_eq              ~> Sup_set_def
  3426 
  3427     listsp_meetI            ~> listsp_infI
  3428     listsp_meet_eq          ~> listsp_inf_eq
  3429 
  3430     meet_min                ~> inf_min
  3431     join_max                ~> sup_max
  3432 
  3433 * Added syntactic class "size"; overloaded constant "size" now has
  3434 type "'a::size ==> bool"
  3435 
  3436 * Internal reorganisation of `size' of datatypes: size theorems
  3437 "foo.size" are no longer subsumed by "foo.simps" (but are still
  3438 simplification rules by default!); theorems "prod.size" now named
  3439 "*.size".
  3440 
  3441 * Class "div" now inherits from class "times" rather than "type".
  3442 INCOMPATIBILITY.
  3443 
  3444 * HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice,
  3445 Linorder etc.  have disappeared; operations defined in terms of
  3446 fold_set now are named Inf_fin, Sup_fin.  INCOMPATIBILITY.
  3447 
  3448 * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
  3449 
  3450 * HOL-Word: New extensive library and type for generic, fixed size
  3451 machine words, with arithemtic, bit-wise, shifting and rotating
  3452 operations, reflection into int, nat, and bool lists, automation for
  3453 linear arithmetic (by automatic reflection into nat or int), including
  3454 lemmas on overflow and monotonicity.  Instantiated to all appropriate
  3455 arithmetic type classes, supporting automatic simplification of
  3456 numerals on all operations.
  3457 
  3458 * Library/Boolean_Algebra: locales for abstract boolean algebras.
  3459 
  3460 * Library/Numeral_Type: numbers as types, e.g. TYPE(32).
  3461 
  3462 * Code generator library theories:
  3463   - Code_Integer represents HOL integers by big integer literals in target
  3464     languages.
  3465   - Code_Char represents HOL characters by character literals in target
  3466     languages.
  3467   - Code_Char_chr like Code_Char, but also offers treatment of character
  3468     codes; includes Code_Integer.
  3469   - Executable_Set allows to generate code for finite sets using lists.
  3470   - Executable_Rat implements rational numbers as triples (sign, enumerator,
  3471     denominator).
  3472   - Executable_Real implements a subset of real numbers, namly those
  3473     representable by rational numbers.
  3474   - Efficient_Nat implements natural numbers by integers, which in general will
  3475     result in higher efficency; pattern matching with 0/Suc is eliminated;
  3476     includes Code_Integer.
  3477   - Code_Index provides an additional datatype index which is mapped to
  3478     target-language built-in integers.
  3479   - Code_Message provides an additional datatype message_string which is isomorphic to
  3480     strings; messages are mapped to target-language strings.
  3481 
  3482 * New package for inductive predicates
  3483 
  3484   An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
  3485 
  3486     inductive
  3487       p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  3488       for z_1 :: U_1 and ... and z_n :: U_m
  3489     where
  3490       rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
  3491     | ...
  3492 
  3493   with full support for type-inference, rather than
  3494 
  3495     consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  3496 
  3497     abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  3498     where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
  3499 
  3500     inductive "s z_1 ... z_m"
  3501     intros
  3502       rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
  3503       ...
  3504 
  3505   For backward compatibility, there is a wrapper allowing inductive
  3506   sets to be defined with the new package via
  3507 
  3508     inductive_set
  3509       s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  3510       for z_1 :: U_1 and ... and z_n :: U_m
  3511     where
  3512       rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
  3513     | ...
  3514 
  3515   or
  3516 
  3517     inductive_set
  3518       s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  3519       and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  3520       for z_1 :: U_1 and ... and z_n :: U_m
  3521     where
  3522       "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
  3523     | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
  3524     | ...
  3525 
  3526   if the additional syntax "p ..." is required.
  3527 
  3528   Numerous examples can be found in the subdirectories src/HOL/Auth,
  3529   src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava.
  3530 
  3531   INCOMPATIBILITIES:
  3532 
  3533   - Since declaration and definition of inductive sets or predicates
  3534     is no longer separated, abbreviations involving the newly
  3535     introduced sets or predicates must be specified together with the
  3536     introduction rules after the 'where' keyword (see above), rather
  3537     than before the actual inductive definition.
  3538 
  3539   - The variables in induction and elimination rules are now
  3540     quantified in the order of their occurrence in the introduction
  3541     rules, rather than in alphabetical order. Since this may break
  3542     some proofs, these proofs either have to be repaired, e.g. by
  3543     reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case'
  3544     statements of the form
  3545 
  3546       case (rule_i a_i_1 ... a_i_{k_i})
  3547 
  3548     or the old order of quantification has to be restored by explicitly adding
  3549     meta-level quantifiers in the introduction rules, i.e.
  3550 
  3551       | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
  3552 
  3553   - The format of the elimination rules is now
  3554 
  3555       p z_1 ... z_m x_1 ... x_n ==>
  3556         (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
  3557         ==> ... ==> P
  3558 
  3559     for predicates and
  3560 
  3561       (x_1, ..., x_n) : s z_1 ... z_m ==>
  3562         (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
  3563         ==> ... ==> P
  3564 
  3565     for sets rather than
  3566 
  3567       x : s z_1 ... z_m ==>
  3568         (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
  3569         ==> ... ==> P
  3570 
  3571     This may require terms in goals to be expanded to n-tuples
  3572     (e.g. using case_tac or simplification with the split_paired_all
  3573     rule) before the above elimination rule is applicable.
  3574 
  3575   - The elimination or case analysis rules for (mutually) inductive
  3576     sets or predicates are now called "p_1.cases" ... "p_k.cases". The
  3577     list of rules "p_1_..._p_k.elims" is no longer available.
  3578 
  3579 * New package "function"/"fun" for general recursive functions,
  3580 supporting mutual and nested recursion, definitions in local contexts,
  3581 more general pattern matching and partiality. See HOL/ex/Fundefs.thy
  3582 for small examples, and the separate tutorial on the function
  3583 package. The old recdef "package" is still available as before, but
  3584 users are encouraged to use the new package.
  3585 
  3586 * Method "lexicographic_order" automatically synthesizes termination
  3587 relations as lexicographic combinations of size measures. 
  3588 
  3589 * Case-expressions allow arbitrary constructor-patterns (including
  3590 "_") and take their order into account, like in functional
  3591 programming.  Internally, this is translated into nested
  3592 case-expressions; missing cases are added and mapped to the predefined
  3593 constant "undefined". In complicated cases printing may no longer show
  3594 the original input but the internal form. Lambda-abstractions allow
  3595 the same form of pattern matching: "% pat1 => e1 | ..." is an
  3596 abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new
  3597 variable.
  3598 
  3599 * IntDef: The constant "int :: nat => int" has been removed; now "int"
  3600 is an abbreviation for "of_nat :: nat => int". The simplification
  3601 rules for "of_nat" have been changed to work like "int" did
  3602 previously.  Potential INCOMPATIBILITY:
  3603   - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
  3604   - of_nat_diff and of_nat_mult are no longer default simp rules
  3605 
  3606 * Method "algebra" solves polynomial equations over (semi)rings using
  3607 Groebner bases. The (semi)ring structure is defined by locales and the
  3608 tool setup depends on that generic context. Installing the method for
  3609 a specific type involves instantiating the locale and possibly adding
  3610 declarations for computation on the coefficients.  The method is
  3611 already instantiated for natural numbers and for the axiomatic class
  3612 of idoms with numerals.  See also the paper by Chaieb and Wenzel at
  3613 CALCULEMUS 2007 for the general principles underlying this
  3614 architecture of context-aware proof-tools.
  3615 
  3616 * Method "ferrack" implements quantifier elimination over
  3617 special-purpose dense linear orders using locales (analogous to
  3618 "algebra"). The method is already installed for class
  3619 {ordered_field,recpower,number_ring} which subsumes real, hyperreal,
  3620 rat, etc.
  3621 
  3622 * Former constant "List.op @" now named "List.append".  Use ML
  3623 antiquotations @{const_name List.append} or @{term " ... @ ... "} to
  3624 circumvent possible incompatibilities when working on ML level.
  3625 
  3626 * primrec: missing cases mapped to "undefined" instead of "arbitrary".
  3627 
  3628 * New function listsum :: 'a list => 'a for arbitrary monoids.
  3629 Special syntax: "SUM x <- xs. f x" (and latex variants)
  3630 
  3631 * New syntax for Haskell-like list comprehension (input only), eg.
  3632 [(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy.
  3633 
  3634 * The special syntax for function "filter" has changed from [x :
  3635 xs. P] to [x <- xs. P] to avoid an ambiguity caused by list
  3636 comprehension syntax, and for uniformity.  INCOMPATIBILITY.
  3637 
  3638 * [a..b] is now defined for arbitrary linear orders.  It used to be
  3639 defined on nat only, as an abbreviation for [a..<Suc b]
  3640 INCOMPATIBILITY.
  3641 
  3642 * Renamed lemma "set_take_whileD"  to "set_takeWhileD".
  3643 
  3644 * New functions "sorted" and "sort" in src/HOL/List.thy.
  3645 
  3646 * New lemma collection field_simps (an extension of ring_simps) for
  3647 manipulating (in)equations involving division. Multiplies with all
  3648 denominators that can be proved to be non-zero (in equations) or
  3649 positive/negative (in inequations).
  3650 
  3651 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib
  3652 have been improved and renamed to ring_simps, group_simps and
  3653 ring_distribs.  Removed lemmas field_xyz in theory Ring_and_Field
  3654 because they were subsumed by lemmas xyz.  INCOMPATIBILITY.
  3655 
  3656 * Theory Library/Commutative_Ring: switched from recdef to function
  3657 package; constants add, mul, pow now curried.  Infix syntax for
  3658 algebraic operations.
  3659 
  3660 * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
  3661 INCOMPATIBILITY.
  3662 
  3663 * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj.
  3664 INCOMPATIBILITY.
  3665 
  3666 * HOL/records: generalised field-update to take a function on the
  3667 field rather than the new value: r(|A := x|) is translated to A_update
  3668 (K x) r The K-combinator that is internally used is called K_record.
  3669 INCOMPATIBILITY: Usage of the plain update functions has to be
  3670 adapted.
  3671  
  3672 * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0
  3673 * x = 0, which are required for a semiring.  Richer structures do not
  3674 inherit from semiring_0 anymore, because this property is a theorem
  3675 there, not an axiom.  INCOMPATIBILITY: In instances of semiring_0,
  3676 there is more to prove, but this is mostly trivial.
  3677 
  3678 * Class "recpower" is generalized to arbitrary monoids, not just
  3679 commutative semirings.  INCOMPATIBILITY: may need to incorporate
  3680 commutativity or semiring properties additionally.
  3681 
  3682 * Constant "List.list_all2" in List.thy now uses authentic syntax.
  3683 INCOMPATIBILITY: translations containing list_all2 may go wrong,
  3684 better use 'abbreviation'.
  3685 
  3686 * Renamed constant "List.op mem" to "List.member".  INCOMPATIBILITY.
  3687 
  3688 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has
  3689 been abandoned in favour of plain 'int'.  INCOMPATIBILITY --
  3690 significant changes for setting up numeral syntax for types:
  3691   - New constants Numeral.pred and Numeral.succ instead
  3692       of former Numeral.bin_pred and Numeral.bin_succ.
  3693   - Use integer operations instead of bin_add, bin_mult and so on.
  3694   - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
  3695   - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
  3696 
  3697 See src/HOL/Integ/IntArith.thy for an example setup.
  3698 
  3699 * Command 'normal_form' computes the normal form of a term that may
  3700 contain free variables.  For example ``normal_form "rev [a, b, c]"''
  3701 produces ``[b, c, a]'' (without proof).  This command is suitable for
  3702 heavy-duty computations because the functions are compiled to ML
  3703 first.  Correspondingly, a method "normalization" is provided.  See
  3704 further src/HOL/ex/NormalForm.thy and src/Tools/nbe.ML.
  3705 
  3706 * Alternative iff syntax "A <-> B" for equality on bool (with priority
  3707 25 like -->); output depends on the "iff" print_mode, the default is
  3708 "A = B" (with priority 50).
  3709 
  3710 * Relations less (<) and less_eq (<=) are also available on type bool.
  3711 Modified syntax to disallow nesting without explicit parentheses,
  3712 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".  Potential
  3713 INCOMPATIBILITY.
  3714 
  3715 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
  3716 
  3717 * Relation composition operator "op O" now has precedence 75 and binds
  3718 stronger than union and intersection. INCOMPATIBILITY.
  3719 
  3720 * The old set interval syntax "{m..n(}" (and relatives) has been
  3721 removed.  Use "{m..<n}" (and relatives) instead.
  3722 
  3723 * In the context of the assumption "~(s = t)" the Simplifier rewrites
  3724 "t = s" to False (by simproc "neq").  INCOMPATIBILITY, consider using
  3725 ``declare [[simproc del: neq]]''.
  3726 
  3727 * Simplifier: "m dvd n" where m and n are numbers is evaluated to
  3728 True/False.
  3729 
  3730 * Theorem Cons_eq_map_conv no longer declared as "simp".
  3731 
  3732 * Theorem setsum_mult renamed to setsum_right_distrib.
  3733 
  3734 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
  3735 ``rule'' method.
  3736 
  3737 * Reimplemented methods "sat" and "satx", with several improvements:
  3738 goals no longer need to be stated as "<prems> ==> False", equivalences
  3739 (i.e. "=" on type bool) are handled, variable names of the form
  3740 "lit_<n>" are no longer reserved, significant speedup.
  3741 
  3742 * Methods "sat" and "satx" can now replay MiniSat proof traces.
  3743 zChaff is still supported as well.
  3744 
  3745 * 'inductive' and 'datatype': provide projections of mutual rules,
  3746 bundled as foo_bar.inducts;
  3747 
  3748 * Library: moved theories Parity, GCD, Binomial, Infinite_Set to
  3749 Library.
  3750 
  3751 * Library: moved theory Accessible_Part to main HOL.
  3752 
  3753 * Library: added theory Coinductive_List of potentially infinite lists
  3754 as greatest fixed-point.
  3755 
  3756 * Library: added theory AssocList which implements (finite) maps as
  3757 association lists.
  3758 
  3759 * Method "evaluation" solves goals (i.e. a boolean expression)
  3760 efficiently by compiling it to ML.  The goal is "proved" (via an
  3761 oracle) if it evaluates to True.
  3762 
  3763 * Linear arithmetic now splits certain operators (e.g. min, max, abs)
  3764 also when invoked by the simplifier.  This results in the Simplifier
  3765 being more powerful on arithmetic goals.  INCOMPATIBILITY.
  3766 Configuration option fast_arith_split_limit=0 recovers the old
  3767 behavior.
  3768 
  3769 * Support for hex (0x20) and binary (0b1001) numerals.
  3770 
  3771 * New method: reify eqs (t), where eqs are equations for an
  3772 interpretation I :: 'a list => 'b => 'c and t::'c is an optional
  3773 parameter, computes a term s::'b and a list xs::'a list and proves the
  3774 theorem I xs s = t. This is also known as reification or quoting. The
  3775 resulting theorem is applied to the subgoal to substitute t with I xs
  3776 s.  If t is omitted, the subgoal itself is reified.
  3777 
  3778 * New method: reflection corr_thm eqs (t). The parameters eqs and (t)
  3779 are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
  3780 where f is supposed to be a computable function (in the sense of code
  3781 generattion). The method uses reify to compute s and xs as above then
  3782 applies corr_thm and uses normalization by evaluation to "prove" f s =
  3783 r and finally gets the theorem t = r, which is again applied to the
  3784 subgoal. An Example is available in src/HOL/ex/ReflectionEx.thy.
  3785 
  3786 * Reflection: Automatic reification now handels binding, an example is
  3787 available in src/HOL/ex/ReflectionEx.thy
  3788 
  3789 * HOL-Statespace: ``State Spaces: The Locale Way'' introduces a
  3790 command 'statespace' that is similar to 'record', but introduces an
  3791 abstract specification based on the locale infrastructure instead of
  3792 HOL types.  This leads to extra flexibility in composing state spaces,
  3793 in particular multiple inheritance and renaming of components.
  3794 
  3795 
  3796 *** HOL-Complex ***
  3797 
  3798 * Hyperreal: Functions root and sqrt are now defined on negative real
  3799 inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x.
  3800 Nonnegativity side conditions have been removed from many lemmas, so
  3801 that more subgoals may now be solved by simplification; potential
  3802 INCOMPATIBILITY.
  3803 
  3804 * Real: new type classes formalize real normed vector spaces and
  3805 algebras, using new overloaded constants scaleR :: real => 'a => 'a
  3806 and norm :: 'a => real.
  3807 
  3808 * Real: constant of_real :: real => 'a::real_algebra_1 injects from
  3809 reals into other types. The overloaded constant Reals :: 'a set is now
  3810 defined as range of_real; potential INCOMPATIBILITY.
  3811 
  3812 * Real: proper support for ML code generation, including 'quickcheck'.
  3813 Reals are implemented as arbitrary precision rationals.
  3814 
  3815 * Hyperreal: Several constants that previously worked only for the
  3816 reals have been generalized, so they now work over arbitrary vector
  3817 spaces. Type annotations may need to be added in some cases; potential
  3818 INCOMPATIBILITY.
  3819 
  3820   Infinitesimal  :: ('a::real_normed_vector) star set
  3821   HFinite        :: ('a::real_normed_vector) star set
  3822   HInfinite      :: ('a::real_normed_vector) star set
  3823   approx         :: ('a::real_normed_vector) star => 'a star => bool
  3824   monad          :: ('a::real_normed_vector) star => 'a star set
  3825   galaxy         :: ('a::real_normed_vector) star => 'a star set
  3826   (NS)LIMSEQ     :: [nat => 'a::real_normed_vector, 'a] => bool
  3827   (NS)convergent :: (nat => 'a::real_normed_vector) => bool
  3828   (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
  3829   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
  3830   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
  3831   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
  3832   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
  3833   sgn            :: 'a::real_normed_vector => 'a
  3834   exp            :: 'a::{recpower,real_normed_field,banach} => 'a
  3835 
  3836 * Complex: Some complex-specific constants are now abbreviations for
  3837 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
  3838 hnorm.  Other constants have been entirely removed in favor of the
  3839 polymorphic versions (INCOMPATIBILITY):
  3840 
  3841   approx        <-- capprox
  3842   HFinite       <-- CFinite
  3843   HInfinite     <-- CInfinite
  3844   Infinitesimal <-- CInfinitesimal
  3845   monad         <-- cmonad
  3846   galaxy        <-- cgalaxy
  3847   (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
  3848   is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
  3849   (ns)deriv     <-- (ns)cderiv
  3850 
  3851 
  3852 *** HOL-Algebra ***
  3853 
  3854 * Formalisation of ideals and the quotient construction over rings.
  3855 
  3856 * Order and lattice theory no longer based on records.
  3857 INCOMPATIBILITY.
  3858 
  3859 * Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
  3860 greatest_closed.  INCOMPATIBILITY.
  3861 
  3862 * Method algebra is now set up via an attribute.  For examples see
  3863 Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
  3864 of algebraic structures.
  3865 
  3866 * Renamed theory CRing to Ring.
  3867 
  3868 
  3869 *** HOL-Nominal ***
  3870 
  3871 * Substantial, yet incomplete support for nominal datatypes (binding
  3872 structures) based on HOL-Nominal logic.  See src/HOL/Nominal and
  3873 src/HOL/Nominal/Examples.  Prospective users should consult
  3874 http://isabelle.in.tum.de/nominal/
  3875 
  3876 
  3877 *** ML ***
  3878 
  3879 * ML basics: just one true type int, which coincides with IntInf.int
  3880 (even on SML/NJ).
  3881 
  3882 * ML within Isar: antiquotations allow to embed statically-checked
  3883 formal entities in the source, referring to the context available at
  3884 compile-time.  For example:
  3885 
  3886 ML {* @{sort "{zero,one}"} *}
  3887 ML {* @{typ "'a => 'b"} *}
  3888 ML {* @{term "%x. x"} *}
  3889 ML {* @{prop "x == y"} *}
  3890 ML {* @{ctyp "'a => 'b"} *}
  3891 ML {* @{cterm "%x. x"} *}
  3892 ML {* @{cprop "x == y"} *}
  3893 ML {* @{thm asm_rl} *}
  3894 ML {* @{thms asm_rl} *}
  3895 ML {* @{type_name c} *}
  3896 ML {* @{type_syntax c} *}
  3897 ML {* @{const_name c} *}
  3898 ML {* @{const_syntax c} *}
  3899 ML {* @{context} *}
  3900 ML {* @{theory} *}
  3901 ML {* @{theory Pure} *}
  3902 ML {* @{theory_ref} *}
  3903 ML {* @{theory_ref Pure} *}
  3904 ML {* @{simpset} *}
  3905 ML {* @{claset} *}
  3906 ML {* @{clasimpset} *}
  3907 
  3908 The same works for sources being ``used'' within an Isar context.
  3909 
  3910 * ML in Isar: improved error reporting; extra verbosity with
  3911 ML_Context.trace enabled.
  3912 
  3913 * Pure/General/table.ML: the join operations now works via exceptions
  3914 DUP/SAME instead of type option. This is simpler in simple cases, and
  3915 admits slightly more efficient complex applications.
  3916 
  3917 * Pure: 'advanced' translation functions (parse_translation etc.) now
  3918 use Context.generic instead of just theory.
  3919 
  3920 * Pure: datatype Context.generic joins theory/Proof.context and
  3921 provides some facilities for code that works in either kind of
  3922 context, notably GenericDataFun for uniform theory and proof data.
  3923 
  3924 * Pure: simplified internal attribute type, which is now always
  3925 Context.generic * thm -> Context.generic * thm. Global (theory) vs.
  3926 local (Proof.context) attributes have been discontinued, while
  3927 minimizing code duplication. Thm.rule_attribute and
  3928 Thm.declaration_attribute build canonical attributes; see also structure
  3929 Context for further operations on Context.generic, notably
  3930 GenericDataFun. INCOMPATIBILITY, need to adapt attribute type
  3931 declarations and definitions.
  3932 
  3933 * Context data interfaces (Theory/Proof/GenericDataFun): removed
  3934 name/print, uninitialized data defaults to ad-hoc copy of empty value,
  3935 init only required for impure data. INCOMPATIBILITY: empty really need
  3936 to be empty (no dependencies on theory content!)
  3937 
  3938 * Pure/kernel: consts certification ignores sort constraints given in
  3939 signature declarations. (This information is not relevant to the
  3940 logic, but only for type inference.) SIGNIFICANT INTERNAL CHANGE,
  3941 potential INCOMPATIBILITY.
  3942 
  3943 * Pure: axiomatic type classes are now purely definitional, with
  3944 explicit proofs of class axioms and super class relations performed
  3945 internally. See Pure/axclass.ML for the main internal interfaces --
  3946 notably AxClass.define_class supercedes AxClass.add_axclass, and
  3947 AxClass.axiomatize_class/classrel/arity supersede
  3948 Sign.add_classes/classrel/arities.
  3949 
  3950 * Pure/Isar: Args/Attrib parsers operate on Context.generic --
  3951 global/local versions on theory vs. Proof.context have been
  3952 discontinued; Attrib.syntax and Method.syntax have been adapted
  3953 accordingly.  INCOMPATIBILITY, need to adapt parser expressions for
  3954 attributes, methods, etc.
  3955 
  3956 * Pure: several functions of signature "... -> theory -> theory * ..."
  3957 have been reoriented to "... -> theory -> ... * theory" in order to
  3958 allow natural usage in combination with the ||>, ||>>, |-> and
  3959 fold_map combinators.
  3960 
  3961 * Pure: official theorem names (closed derivations) and additional
  3962 comments (tags) are now strictly separate.  Name hints -- which are
  3963 maintained as tags -- may be attached any time without affecting the
  3964 derivation.
  3965 
  3966 * Pure: primitive rule lift_rule now takes goal cterm instead of an
  3967 actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
  3968 achieve the old behaviour.
  3969 
  3970 * Pure: the "Goal" constant is now called "prop", supporting a
  3971 slightly more general idea of ``protecting'' meta-level rule
  3972 statements.
  3973 
  3974 * Pure: Logic.(un)varify only works in a global context, which is now
  3975 enforced instead of silently assumed.  INCOMPATIBILITY, may use
  3976 Logic.legacy_(un)varify as temporary workaround.
  3977 
  3978 * Pure: structure Name provides scalable operations for generating
  3979 internal variable names, notably Name.variants etc.  This replaces
  3980 some popular functions from term.ML:
  3981 
  3982   Term.variant		->  Name.variant
  3983   Term.variantlist	->  Name.variant_list
  3984   Term.invent_names	->  Name.invent_list
  3985 
  3986 Note that low-level renaming rarely occurs in new code -- operations
  3987 from structure Variable are used instead (see below).
  3988 
  3989 * Pure: structure Variable provides fundamental operations for proper
  3990 treatment of fixed/schematic variables in a context.  For example,
  3991 Variable.import introduces fixes for schematics of given facts and
  3992 Variable.export reverses the effect (up to renaming) -- this replaces
  3993 various freeze_thaw operations.
  3994 
  3995 * Pure: structure Goal provides simple interfaces for
  3996 init/conclude/finish and tactical prove operations (replacing former
  3997 Tactic.prove).  Goal.prove is the canonical way to prove results
  3998 within a given context; Goal.prove_global is a degraded version for
  3999 theory level goals, including a global Drule.standard.  Note that
  4000 OldGoals.prove_goalw_cterm has long been obsolete, since it is
  4001 ill-behaved in a local proof context (e.g. with local fixes/assumes or
  4002 in a locale context).
  4003 
  4004 * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.)
  4005 and type checking (Syntax.check_term etc.), with common combinations
  4006 (Syntax.read_term etc.). These supersede former Sign.read_term etc.
  4007 which are considered legacy and await removal.
  4008 
  4009 * Pure/Syntax: generic interfaces for type unchecking
  4010 (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
  4011 with common combinations (Syntax.pretty_term, Syntax.string_of_term
  4012 etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
  4013 available for convenience, but refer to the very same operations using
  4014 a mere theory instead of a full context.
  4015 
  4016 * Isar: simplified treatment of user-level errors, using exception
  4017 ERROR of string uniformly.  Function error now merely raises ERROR,
  4018 without any side effect on output channels.  The Isar toplevel takes
  4019 care of proper display of ERROR exceptions.  ML code may use plain
  4020 handle/can/try; cat_error may be used to concatenate errors like this:
  4021 
  4022   ... handle ERROR msg => cat_error msg "..."
  4023 
  4024 Toplevel ML code (run directly or through the Isar toplevel) may be
  4025 embedded into the Isar toplevel with exception display/debug like
  4026 this:
  4027 
  4028   Isar.toplevel (fn () => ...)
  4029 
  4030 INCOMPATIBILITY, removed special transform_error facilities, removed
  4031 obsolete variants of user-level exceptions (ERROR_MESSAGE,
  4032 Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
  4033 -- use plain ERROR instead.
  4034 
  4035 * Isar: theory setup now has type (theory -> theory), instead of a
  4036 list.  INCOMPATIBILITY, may use #> to compose setup functions.
  4037 
  4038 * Isar: ML toplevel pretty printer for type Proof.context, subject to
  4039 ProofContext.debug/verbose flags.
  4040 
  4041 * Isar: Toplevel.theory_to_proof admits transactions that modify the
  4042 theory before entering a proof state.  Transactions now always see a
  4043 quasi-functional intermediate checkpoint, both in interactive and
  4044 batch mode.
  4045 
  4046 * Isar: simplified interfaces for outer syntax.  Renamed
  4047 OuterSyntax.add_keywords to OuterSyntax.keywords.  Removed
  4048 OuterSyntax.add_parsers -- this functionality is now included in
  4049 OuterSyntax.command etc.  INCOMPATIBILITY.
  4050 
  4051 * Simplifier: the simpset of a running simplification process now
  4052 contains a proof context (cf. Simplifier.the_context), which is the
  4053 very context that the initial simpset has been retrieved from (by
  4054 simpset_of/local_simpset_of).  Consequently, all plug-in components
  4055 (solver, looper etc.) may depend on arbitrary proof data.
  4056 
  4057 * Simplifier.inherit_context inherits the proof context (plus the
  4058 local bounds) of the current simplification process; any simproc
  4059 etc. that calls the Simplifier recursively should do this!  Removed
  4060 former Simplifier.inherit_bounds, which is already included here --
  4061 INCOMPATIBILITY.  Tools based on low-level rewriting may even have to
  4062 specify an explicit context using Simplifier.context/theory_context.
  4063 
  4064 * Simplifier/Classical Reasoner: more abstract interfaces
  4065 change_simpset/claset for modifying the simpset/claset reference of a
  4066 theory; raw versions simpset/claset_ref etc. have been discontinued --
  4067 INCOMPATIBILITY.
  4068 
  4069 * Provers: more generic wrt. syntax of object-logics, avoid hardwired
  4070 "Trueprop" etc.
  4071 
  4072 
  4073 *** System ***
  4074 
  4075 * settings: the default heap location within ISABELLE_HOME_USER now
  4076 includes ISABELLE_IDENTIFIER.  This simplifies use of multiple
  4077 Isabelle installations.
  4078 
  4079 * isabelle-process: option -S (secure mode) disables some critical
  4080 operations, notably runtime compilation and evaluation of ML source
  4081 code.
  4082 
  4083 * Basic Isabelle mode for jEdit, see Isabelle/lib/jedit/.
  4084 
  4085 * Support for parallel execution, using native multicore support of
  4086 Poly/ML 5.1.  The theory loader exploits parallelism when processing
  4087 independent theories, according to the given theory header
  4088 specifications. The maximum number of worker threads is specified via
  4089 usedir option -M or the "max-threads" setting in Proof General. A
  4090 speedup factor of 1.5--3.5 can be expected on a 4-core machine, and up
  4091 to 6 on a 8-core machine.  User-code needs to observe certain
  4092 guidelines for thread-safe programming, see appendix A in the Isar
  4093 Implementation manual.
  4094 
  4095 
  4096 
  4097 New in Isabelle2005 (October 2005)
  4098 ----------------------------------
  4099 
  4100 *** General ***
  4101 
  4102 * Theory headers: the new header syntax for Isar theories is
  4103 
  4104   theory <name>
  4105   imports <theory1> ... <theoryN>
  4106   uses <file1> ... <fileM>
  4107   begin
  4108 
  4109 where the 'uses' part is optional.  The previous syntax
  4110 
  4111   theory <name> = <theory1> + ... + <theoryN>:
  4112 
  4113 will disappear in the next release.  Use isatool fixheaders to convert
  4114 existing theory files.  Note that there is no change in ancient
  4115 non-Isar theories now, but these will disappear soon.
  4116 
  4117 * Theory loader: parent theories can now also be referred to via
  4118 relative and absolute paths.
  4119 
  4120 * Command 'find_theorems' searches for a list of criteria instead of a
  4121 list of constants. Known criteria are: intro, elim, dest, name:string,
  4122 simp:term, and any term. Criteria can be preceded by '-' to select
  4123 theorems that do not match. Intro, elim, dest select theorems that
  4124 match the current goal, name:s selects theorems whose fully qualified
  4125 name contain s, and simp:term selects all simplification rules whose
  4126 lhs match term.  Any other term is interpreted as pattern and selects
  4127 all theorems matching the pattern. Available in ProofGeneral under
  4128 'ProofGeneral -> Find Theorems' or C-c C-f.  Example:
  4129 
  4130   C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."
  4131 
  4132 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
  4133 matching the current goal as introduction rule and not having "HOL."
  4134 in their name (i.e. not being defined in theory HOL).
  4135 
  4136 * Command 'thms_containing' has been discontinued in favour of
  4137 'find_theorems'; INCOMPATIBILITY.
  4138 
  4139 * Communication with Proof General is now 8bit clean, which means that
  4140 Unicode text in UTF-8 encoding may be used within theory texts (both
  4141 formal and informal parts).  Cf. option -U of the Isabelle Proof
  4142 General interface.  Here are some simple examples (cf. src/HOL/ex):
  4143 
  4144   http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html
  4145   http://isabelle.in.tum.de/library/HOL/ex/Chinese.html
  4146 
  4147 * Improved efficiency of the Simplifier and, to a lesser degree, the
  4148 Classical Reasoner.  Typical big applications run around 2 times
  4149 faster.
  4150 
  4151 
  4152 *** Document preparation ***
  4153 
  4154 * Commands 'display_drafts' and 'print_drafts' perform simple output
  4155 of raw sources.  Only those symbols that do not require additional
  4156 LaTeX packages (depending on comments in isabellesym.sty) are
  4157 displayed properly, everything else is left verbatim.  isatool display
  4158 and isatool print are used as front ends (these are subject to the
  4159 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
  4160 
  4161 * Command tags control specific markup of certain regions of text,
  4162 notably folding and hiding.  Predefined tags include "theory" (for
  4163 theory begin and end), "proof" for proof commands, and "ML" for
  4164 commands involving ML code; the additional tags "visible" and
  4165 "invisible" are unused by default.  Users may give explicit tag
  4166 specifications in the text, e.g. ''by %invisible (auto)''.  The
  4167 interpretation of tags is determined by the LaTeX job during document
  4168 preparation: see option -V of isatool usedir, or options -n and -t of
  4169 isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
  4170 \isadroptag.
  4171 
  4172 Several document versions may be produced at the same time via isatool
  4173 usedir (the generated index.html will link all of them).  Typical
  4174 specifications include ''-V document=theory,proof,ML'' to present
  4175 theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
  4176 proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
  4177 these parts without any formal replacement text.  The Isabelle site
  4178 default settings produce ''document'' and ''outline'' versions as
  4179 specified above.
  4180 
  4181 * Several new antiquotations:
  4182 
  4183   @{term_type term} prints a term with its type annotated;
  4184 
  4185   @{typeof term} prints the type of a term;
  4186 
  4187   @{const const} is the same as @{term const}, but checks that the
  4188   argument is a known logical constant;
  4189 
  4190   @{term_style style term} and @{thm_style style thm} print a term or
  4191   theorem applying a "style" to it
  4192 
  4193   @{ML text}
  4194 
  4195 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
  4196 definitions, equations, inequations etc., 'concl' printing only the
  4197 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19'
  4198 to print the specified premise.  TermStyle.add_style provides an ML
  4199 interface for introducing further styles.  See also the "LaTeX Sugar"
  4200 document practical applications.  The ML antiquotation prints
  4201 type-checked ML expressions verbatim.
  4202 
  4203 * Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
  4204 and 'text' support optional locale specification '(in loc)', which
  4205 specifies the default context for interpreting antiquotations.  For
  4206 example: 'text (in lattice) {* @{thm inf_assoc}*}'.
  4207 
  4208 * Option 'locale=NAME' of antiquotations specifies an alternative
  4209 context interpreting the subsequent argument.  For example: @{thm
  4210 [locale=lattice] inf_assoc}.
  4211 
  4212 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
  4213 a proof context.
  4214 
  4215 * Proper output of antiquotations for theory commands involving a
  4216 proof context (such as 'locale' or 'theorem (in loc) ...').
  4217 
  4218 * Delimiters of outer tokens (string etc.) now produce separate LaTeX
  4219 macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
  4220 
  4221 * isatool usedir: new option -C (default true) controls whether option
  4222 -D should include a copy of the original document directory; -C false
  4223 prevents unwanted effects such as copying of administrative CVS data.
  4224 
  4225 
  4226 *** Pure ***
  4227 
  4228 * Considerably improved version of 'constdefs' command.  Now performs
  4229 automatic type-inference of declared constants; additional support for
  4230 local structure declarations (cf. locales and HOL records), see also
  4231 isar-ref manual.  Potential INCOMPATIBILITY: need to observe strictly
  4232 sequential dependencies of definitions within a single 'constdefs'
  4233 section; moreover, the declared name needs to be an identifier.  If
  4234 all fails, consider to fall back on 'consts' and 'defs' separately.
  4235 
  4236 * Improved indexed syntax and implicit structures.  First of all,
  4237 indexed syntax provides a notational device for subscripted
  4238 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
  4239 expressions.  Secondly, in a local context with structure
  4240 declarations, number indexes \<^sub>n or the empty index (default
  4241 number 1) refer to a certain fixed variable implicitly; option
  4242 show_structs controls printing of implicit structures.  Typical
  4243 applications of these concepts involve record types and locales.
  4244 
  4245 * New command 'no_syntax' removes grammar declarations (and
  4246 translations) resulting from the given syntax specification, which is
  4247 interpreted in the same manner as for the 'syntax' command.
  4248 
  4249 * 'Advanced' translation functions (parse_translation etc.) may depend
  4250 on the signature of the theory context being presently used for
  4251 parsing/printing, see also isar-ref manual.
  4252 
  4253 * Improved 'oracle' command provides a type-safe interface to turn an
  4254 ML expression of type theory -> T -> term into a primitive rule of
  4255 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
  4256 is already included here); see also FOL/ex/IffExample.thy;
  4257 INCOMPATIBILITY.
  4258 
  4259 * axclass: name space prefix for class "c" is now "c_class" (was "c"
  4260 before); "cI" is no longer bound, use "c.intro" instead.
  4261 INCOMPATIBILITY.  This change avoids clashes of fact bindings for
  4262 axclasses vs. locales.
  4263 
  4264 * Improved internal renaming of symbolic identifiers -- attach primes
  4265 instead of base 26 numbers.
  4266 
  4267 * New flag show_question_marks controls printing of leading question
  4268 marks in schematic variable names.
  4269 
  4270 * In schematic variable names, *any* symbol following \<^isub> or
  4271 \<^isup> is now treated as part of the base name.  For example, the
  4272 following works without printing of awkward ".0" indexes:
  4273 
  4274   lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"
  4275     by simp
  4276 
  4277 * Inner syntax includes (*(*nested*) comments*).
  4278 
  4279 * Pretty printer now supports unbreakable blocks, specified in mixfix
  4280 annotations as "(00...)".
  4281 
  4282 * Clear separation of logical types and nonterminals, where the latter
  4283 may only occur in 'syntax' specifications or type abbreviations.
  4284 Before that distinction was only partially implemented via type class
  4285 "logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper
  4286 use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very
  4287 exotic syntax specifications may require further adaption
  4288 (e.g. Cube/Cube.thy).
  4289 
  4290 * Removed obsolete type class "logic", use the top sort {} instead.
  4291 Note that non-logical types should be declared as 'nonterminals'
  4292 rather than 'types'.  INCOMPATIBILITY for new object-logic
  4293 specifications.
  4294 
  4295 * Attributes 'induct' and 'cases': type or set names may now be
  4296 locally fixed variables as well.
  4297 
  4298 * Simplifier: can now control the depth to which conditional rewriting
  4299 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
  4300 Limit.
  4301 
  4302 * Simplifier: simplification procedures may now take the current
  4303 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
  4304 interface), which is very useful for calling the Simplifier
  4305 recursively.  Minor INCOMPATIBILITY: the 'prems' argument of simprocs
  4306 is gone -- use prems_of_ss on the simpset instead.  Moreover, the
  4307 low-level mk_simproc no longer applies Logic.varify internally, to
  4308 allow for use in a context of fixed variables.
  4309 
  4310 * thin_tac now works even if the assumption being deleted contains !!
  4311 or ==>.  More generally, erule now works even if the major premise of
  4312 the elimination rule contains !! or ==>.
  4313 
  4314 * Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY.
  4315 
  4316 * Reorganized bootstrapping of the Pure theories; CPure is now derived
  4317 from Pure, which contains all common declarations already.  Both
  4318 theories are defined via plain Isabelle/Isar .thy files.
  4319 INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
  4320 CPure.elim / CPure.dest attributes) now appear in the Pure name space;
  4321 use isatool fixcpure to adapt your theory and ML sources.
  4322 
  4323 * New syntax 'name(i-j, i-, i, ...)' for referring to specific
  4324 selections of theorems in named facts via index ranges.
  4325 
  4326 * 'print_theorems': in theory mode, really print the difference
  4327 wrt. the last state (works for interactive theory development only),
  4328 in proof mode print all local facts (cf. 'print_facts');
  4329 
  4330 * 'hide': option '(open)' hides only base names.
  4331 
  4332 * More efficient treatment of intermediate checkpoints in interactive
  4333 theory development.
  4334 
  4335 * Code generator is now invoked via code_module (incremental code
  4336 generation) and code_library (modular code generation, ML structures
  4337 for each theory).  INCOMPATIBILITY: new keywords 'file' and 'contains'
  4338 must be quoted when used as identifiers.
  4339 
  4340 * New 'value' command for reading, evaluating and printing terms using
  4341 the code generator.  INCOMPATIBILITY: command keyword 'value' must be
  4342 quoted when used as identifier.
  4343 
  4344 
  4345 *** Locales ***
  4346 
  4347 * New commands for the interpretation of locale expressions in
  4348 theories (1), locales (2) and proof contexts (3).  These generate
  4349 proof obligations from the expression specification.  After the
  4350 obligations have been discharged, theorems of the expression are added
  4351 to the theory, target locale or proof context.  The synopsis of the
  4352 commands is a follows:
  4353 
  4354   (1) interpretation expr inst
  4355   (2) interpretation target < expr
  4356   (3) interpret expr inst
  4357 
  4358 Interpretation in theories and proof contexts require a parameter
  4359 instantiation of terms from the current context.  This is applied to
  4360 specifications and theorems of the interpreted expression.
  4361 Interpretation in locales only permits parameter renaming through the
  4362 locale expression.  Interpretation is smart in that interpretations
  4363 that are active already do not occur in proof obligations, neither are
  4364 instantiated theorems stored in duplicate.  Use 'print_interps' to
  4365 inspect active interpretations of a particular locale.  For details,
  4366 see the Isar Reference manual.  Examples can be found in
  4367 HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy.
  4368 
  4369 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
  4370 'interpret' instead.
  4371 
  4372 * New context element 'constrains' for adding type constraints to
  4373 parameters.
  4374 
  4375 * Context expressions: renaming of parameters with syntax
  4376 redeclaration.
  4377 
  4378 * Locale declaration: 'includes' disallowed.
  4379 
  4380 * Proper static binding of attribute syntax -- i.e. types / terms /
  4381 facts mentioned as arguments are always those of the locale definition
  4382 context, independently of the context of later invocations.  Moreover,
  4383 locale operations (renaming and type / term instantiation) are applied
  4384 to attribute arguments as expected.
  4385 
  4386 INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of
  4387 actual attributes; rare situations may require Attrib.attribute to
  4388 embed those attributes into Attrib.src that lack concrete syntax.
  4389 Attribute implementations need to cooperate properly with the static
  4390 binding mechanism.  Basic parsers Args.XXX_typ/term/prop and
  4391 Attrib.XXX_thm etc. already do the right thing without further
  4392 intervention.  Only unusual applications -- such as "where" or "of"
  4393 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both
  4394 on the context and the facts involved -- may have to assign parsed
  4395 values to argument tokens explicitly.
  4396 
  4397 * Changed parameter management in theorem generation for long goal
  4398 statements with 'includes'.  INCOMPATIBILITY: produces a different
  4399 theorem statement in rare situations.
  4400 
  4401 * Locale inspection command 'print_locale' omits notes elements.  Use
  4402 'print_locale!' to have them included in the output.
  4403 
  4404 
  4405 *** Provers ***
  4406 
  4407 * Provers/hypsubst.ML: improved version of the subst method, for
  4408 single-step rewriting: it now works in bound variable contexts. New is
  4409 'subst (asm)', for rewriting an assumption.  INCOMPATIBILITY: may
  4410 rewrite a different subterm than the original subst method, which is
  4411 still available as 'simplesubst'.
  4412 
  4413 * Provers/quasi.ML: new transitivity reasoners for transitivity only
  4414 and quasi orders.
  4415 
  4416 * Provers/trancl.ML: new transitivity reasoner for transitive and
  4417 reflexive-transitive closure of relations.
  4418 
  4419 * Provers/blast.ML: new reference depth_limit to make blast's depth
  4420 limit (previously hard-coded with a value of 20) user-definable.
  4421 
  4422 * Provers/simplifier.ML has been moved to Pure, where Simplifier.setup
  4423 is peformed already.  Object-logics merely need to finish their
  4424 initial simpset configuration as before.  INCOMPATIBILITY.
  4425 
  4426 
  4427 *** HOL ***
  4428 
  4429 * Symbolic syntax of Hilbert Choice Operator is now as follows:
  4430 
  4431   syntax (epsilon)
  4432     "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
  4433 
  4434 The symbol \<some> is displayed as the alternative epsilon of LaTeX
  4435 and x-symbol; use option '-m epsilon' to get it actually printed.
  4436 Moreover, the mathematically important symbolic identifier \<epsilon>
  4437 becomes available as variable, constant etc.  INCOMPATIBILITY,
  4438 
  4439 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
  4440 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
  4441 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
  4442 support corresponding Isar calculations.
  4443 
  4444 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
  4445 instead of ":".
  4446 
  4447 * theory SetInterval: changed the syntax for open intervals:
  4448 
  4449   Old       New
  4450   {..n(}    {..<n}
  4451   {)n..}    {n<..}
  4452   {m..n(}   {m..<n}
  4453   {)m..n}   {m<..n}
  4454   {)m..n(}  {m<..<n}
  4455 
  4456 The old syntax is still supported but will disappear in the next
  4457 release.  For conversion use the following Emacs search and replace
  4458 patterns (these are not perfect but work quite well):
  4459 
  4460   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
  4461   \.\.\([^(}]*\)(}  ->  \.\.<\1}
  4462 
  4463 * Theory Commutative_Ring (in Library): method comm_ring for proving
  4464 equalities in commutative rings; method 'algebra' provides a generic
  4465 interface.
  4466 
  4467 * Theory Finite_Set: changed the syntax for 'setsum', summation over
  4468 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
  4469 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
  4470 be a tuple pattern.
  4471 
  4472 Some new syntax forms are available:
  4473 
  4474   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
  4475   "\<Sum>x = a..b. e"   for     "setsum (%x. e) {a..b}"
  4476   "\<Sum>x = a..<b. e"  for     "setsum (%x. e) {a..<b}"
  4477   "\<Sum>x < k. e"      for     "setsum (%x. e) {..<k}"
  4478 
  4479 The latter form "\<Sum>x < k. e" used to be based on a separate
  4480 function "Summation", which has been discontinued.
  4481 
  4482 * theory Finite_Set: in structured induction proofs, the insert case
  4483 is now 'case (insert x F)' instead of the old counterintuitive 'case
  4484 (insert F x)'.
  4485 
  4486 * The 'refute' command has been extended to support a much larger
  4487 fragment of HOL, including axiomatic type classes, constdefs and
  4488 typedefs, inductive datatypes and recursion.
  4489 
  4490 * New tactics 'sat' and 'satx' to prove propositional tautologies.
  4491 Requires zChaff with proof generation to be installed.  See
  4492 HOL/ex/SAT_Examples.thy for examples.
  4493 
  4494 * Datatype induction via method 'induct' now preserves the name of the
  4495 induction variable. For example, when proving P(xs::'a list) by
  4496 induction on xs, the induction step is now P(xs) ==> P(a#xs) rather
  4497 than P(list) ==> P(a#list) as previously.  Potential INCOMPATIBILITY
  4498 in unstructured proof scripts.
  4499 
  4500 * Reworked implementation of records.  Improved scalability for
  4501 records with many fields, avoiding performance problems for type
  4502 inference. Records are no longer composed of nested field types, but
  4503 of nested extension types. Therefore the record type only grows linear
  4504 in the number of extensions and not in the number of fields.  The
  4505 top-level (users) view on records is preserved.  Potential
  4506 INCOMPATIBILITY only in strange cases, where the theory depends on the
  4507 old record representation. The type generated for a record is called
  4508 <record_name>_ext_type.
  4509 
  4510 Flag record_quick_and_dirty_sensitive can be enabled to skip the
  4511 proofs triggered by a record definition or a simproc (if
  4512 quick_and_dirty is enabled).  Definitions of large records can take
  4513 quite long.
  4514 
  4515 New simproc record_upd_simproc for simplification of multiple record
  4516 updates enabled by default.  Moreover, trivial updates are also
  4517 removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
  4518 occasionally, since simplification is more powerful by default.
  4519 
  4520 * typedef: proper support for polymorphic sets, which contain extra
  4521 type-variables in the term.
  4522 
  4523 * Simplifier: automatically reasons about transitivity chains
  4524 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
  4525 provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY:
  4526 old proofs break occasionally as simplification may now solve more
  4527 goals than previously.
  4528 
  4529 * Simplifier: converts x <= y into x = y if assumption y <= x is
  4530 present.  Works for all partial orders (class "order"), in particular
  4531 numbers and sets.  For linear orders (e.g. numbers) it treats ~ x < y
  4532 just like y <= x.
  4533 
  4534 * Simplifier: new simproc for "let x = a in f x".  If a is a free or
  4535 bound variable or a constant then the let is unfolded.  Otherwise
  4536 first a is simplified to b, and then f b is simplified to g. If
  4537 possible we abstract b from g arriving at "let x = b in h x",
  4538 otherwise we unfold the let and arrive at g.  The simproc can be
  4539 enabled/disabled by the reference use_let_simproc.  Potential
  4540 INCOMPATIBILITY since simplification is more powerful by default.
  4541 
  4542 * Classical reasoning: the meson method now accepts theorems as arguments.
  4543 
  4544 * Prover support: pre-release of the Isabelle-ATP linkup, which runs background
  4545 jobs to provide advice on the provability of subgoals.
  4546 
  4547 * Theory OrderedGroup and Ring_and_Field: various additions and
  4548 improvements to faciliate calculations involving equalities and
  4549 inequalities.
  4550 
  4551 The following theorems have been eliminated or modified
  4552 (INCOMPATIBILITY):
  4553 
  4554   abs_eq             now named abs_of_nonneg
  4555   abs_of_ge_0        now named abs_of_nonneg
  4556   abs_minus_eq       now named abs_of_nonpos
  4557   imp_abs_id         now named abs_of_nonneg
  4558   imp_abs_neg_id     now named abs_of_nonpos
  4559   mult_pos           now named mult_pos_pos
  4560   mult_pos_le        now named mult_nonneg_nonneg
  4561   mult_pos_neg_le    now named mult_nonneg_nonpos
  4562   mult_pos_neg2_le   now named mult_nonneg_nonpos2
  4563   mult_neg           now named mult_neg_neg
  4564   mult_neg_le        now named mult_nonpos_nonpos
  4565 
  4566 * The following lemmas in Ring_and_Field have been added to the simplifier:
  4567      
  4568      zero_le_square
  4569      not_square_less_zero 
  4570 
  4571   The following lemmas have been deleted from Real/RealPow:
  4572   
  4573      realpow_zero_zero
  4574      realpow_two
  4575      realpow_less
  4576      zero_le_power
  4577      realpow_two_le
  4578      abs_realpow_two
  4579      realpow_two_abs     
  4580 
  4581 * Theory Parity: added rules for simplifying exponents.
  4582 
  4583 * Theory List:
  4584 
  4585 The following theorems have been eliminated or modified
  4586 (INCOMPATIBILITY):
  4587 
  4588   list_all_Nil       now named list_all.simps(1)
  4589   list_all_Cons      now named list_all.simps(2)
  4590   list_all_conv      now named list_all_iff
  4591   set_mem_eq         now named mem_iff
  4592 
  4593 * Theories SetsAndFunctions and BigO (see HOL/Library) support
  4594 asymptotic "big O" calculations.  See the notes in BigO.thy.
  4595 
  4596 
  4597 *** HOL-Complex ***
  4598 
  4599 * Theory RealDef: better support for embedding natural numbers and
  4600 integers in the reals.
  4601 
  4602 The following theorems have been eliminated or modified
  4603 (INCOMPATIBILITY):
  4604 
  4605   exp_ge_add_one_self  now requires no hypotheses
  4606   real_of_int_add      reversed direction of equality (use [symmetric])
  4607   real_of_int_minus    reversed direction of equality (use [symmetric])
  4608   real_of_int_diff     reversed direction of equality (use [symmetric])
  4609   real_of_int_mult     reversed direction of equality (use [symmetric])
  4610 
  4611 * Theory RComplete: expanded support for floor and ceiling functions.
  4612 
  4613 * Theory Ln is new, with properties of the natural logarithm
  4614 
  4615 * Hyperreal: There is a new type constructor "star" for making
  4616 nonstandard types.  The old type names are now type synonyms:
  4617 
  4618   hypreal = real star
  4619   hypnat = nat star
  4620   hcomplex = complex star
  4621 
  4622 * Hyperreal: Many groups of similarly-defined constants have been
  4623 replaced by polymorphic versions (INCOMPATIBILITY):
  4624 
  4625   star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex
  4626 
  4627   starset      <-- starsetNat, starsetC
  4628   *s*          <-- *sNat*, *sc*
  4629   starset_n    <-- starsetNat_n, starsetC_n
  4630   *sn*         <-- *sNatn*, *scn*
  4631   InternalSets <-- InternalNatSets, InternalCSets
  4632 
  4633   starfun      <-- starfun{Nat,Nat2,C,RC,CR}
  4634   *f*          <-- *fNat*, *fNat2*, *fc*, *fRc*, *fcR*
  4635   starfun_n    <-- starfun{Nat,Nat2,C,RC,CR}_n
  4636   *fn*         <-- *fNatn*, *fNat2n*, *fcn*, *fRcn*, *fcRn*
  4637   InternalFuns <-- InternalNatFuns, InternalNatFuns2, Internal{C,RC,CR}Funs
  4638 
  4639 * Hyperreal: Many type-specific theorems have been removed in favor of
  4640 theorems specific to various axiomatic type classes (INCOMPATIBILITY):
  4641 
  4642   add_commute <-- {hypreal,hypnat,hcomplex}_add_commute
  4643   add_assoc   <-- {hypreal,hypnat,hcomplex}_add_assocs
  4644   OrderedGroup.add_0 <-- {hypreal,hypnat,hcomplex}_add_zero_left
  4645   OrderedGroup.add_0_right <-- {hypreal,hcomplex}_add_zero_right
  4646   right_minus <-- hypreal_add_minus
  4647   left_minus <-- {hypreal,hcomplex}_add_minus_left
  4648   mult_commute <-- {hypreal,hypnat,hcomplex}_mult_commute
  4649   mult_assoc <-- {hypreal,hypnat,hcomplex}_mult_assoc
  4650   mult_1_left <-- {hypreal,hypnat}_mult_1, hcomplex_mult_one_left
  4651   mult_1_right <-- hcomplex_mult_one_right
  4652   mult_zero_left <-- hcomplex_mult_zero_left
  4653   left_distrib <-- {hypreal,hypnat,hcomplex}_add_mult_distrib
  4654   right_distrib <-- hypnat_add_mult_distrib2
  4655   zero_neq_one <-- {hypreal,hypnat,hcomplex}_zero_not_eq_one
  4656   right_inverse <-- hypreal_mult_inverse
  4657   left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left
  4658   order_refl <-- {hypreal,hypnat}_le_refl
  4659   order_trans <-- {hypreal,hypnat}_le_trans
  4660   order_antisym <-- {hypreal,hypnat}_le_anti_sym
  4661   order_less_le <-- {hypreal,hypnat}_less_le
  4662   linorder_linear <-- {hypreal,hypnat}_le_linear
  4663   add_left_mono <-- {hypreal,hypnat}_add_left_mono
  4664   mult_strict_left_mono <-- {hypreal,hypnat}_mult_less_mono2
  4665   add_nonneg_nonneg <-- hypreal_le_add_order
  4666 
  4667 * Hyperreal: Separate theorems having to do with type-specific
  4668 versions of constants have been merged into theorems that apply to the
  4669 new polymorphic constants (INCOMPATIBILITY):
  4670 
  4671   STAR_UNIV_set <-- {STAR_real,NatStar_real,STARC_complex}_set
  4672   STAR_empty_set <-- {STAR,NatStar,STARC}_empty_set
  4673   STAR_Un <-- {STAR,NatStar,STARC}_Un
  4674   STAR_Int <-- {STAR,NatStar,STARC}_Int
  4675   STAR_Compl <-- {STAR,NatStar,STARC}_Compl
  4676   STAR_subset <-- {STAR,NatStar,STARC}_subset
  4677   STAR_mem <-- {STAR,NatStar,STARC}_mem
  4678   STAR_mem_Compl <-- {STAR,STARC}_mem_Compl
  4679   STAR_diff <-- {STAR,STARC}_diff
  4680   STAR_star_of_image_subset <-- {STAR_hypreal_of_real, NatStar_hypreal_of_real,
  4681     STARC_hcomplex_of_complex}_image_subset
  4682   starset_n_Un <-- starset{Nat,C}_n_Un
  4683   starset_n_Int <-- starset{Nat,C}_n_Int
  4684   starset_n_Compl <-- starset{Nat,C}_n_Compl
  4685   starset_n_diff <-- starset{Nat,C}_n_diff
  4686   InternalSets_Un <-- Internal{Nat,C}Sets_Un
  4687   InternalSets_Int <-- Internal{Nat,C}Sets_Int
  4688   InternalSets_Compl <-- Internal{Nat,C}Sets_Compl
  4689   InternalSets_diff <-- Internal{Nat,C}Sets_diff
  4690   InternalSets_UNIV_diff <-- Internal{Nat,C}Sets_UNIV_diff
  4691   InternalSets_starset_n <-- Internal{Nat,C}Sets_starset{Nat,C}_n
  4692   starset_starset_n_eq <-- starset{Nat,C}_starset{Nat,C}_n_eq
  4693   starset_n_starset <-- starset{Nat,C}_n_starset{Nat,C}
  4694   starfun_n_starfun <-- starfun{Nat,Nat2,C,RC,CR}_n_starfun{Nat,Nat2,C,RC,CR}
  4695   starfun <-- starfun{Nat,Nat2,C,RC,CR}
  4696   starfun_mult <-- starfun{Nat,Nat2,C,RC,CR}_mult
  4697   starfun_add <-- starfun{Nat,Nat2,C,RC,CR}_add
  4698   starfun_minus <-- starfun{Nat,Nat2,C,RC,CR}_minus
  4699   starfun_diff <-- starfun{C,RC,CR}_diff
  4700   starfun_o <-- starfun{NatNat2,Nat2,_stafunNat,C,C_starfunRC,_starfunCR}_o
  4701   starfun_o2 <-- starfun{NatNat2,_stafunNat,C,C_starfunRC,_starfunCR}_o2
  4702   starfun_const_fun <-- starfun{Nat,Nat2,C,RC,CR}_const_fun
  4703   starfun_inverse <-- starfun{Nat,C,RC,CR}_inverse
  4704   starfun_eq <-- starfun{Nat,Nat2,C,RC,CR}_eq
  4705   starfun_eq_iff <-- starfun{C,RC,CR}_eq_iff
  4706   starfun_Id <-- starfunC_Id
  4707   starfun_approx <-- starfun{Nat,CR}_approx
  4708   starfun_capprox <-- starfun{C,RC}_capprox
  4709   starfun_abs <-- starfunNat_rabs
  4710   starfun_lambda_cancel <-- starfun{C,CR,RC}_lambda_cancel
  4711   starfun_lambda_cancel2 <-- starfun{C,CR,RC}_lambda_cancel2
  4712   starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox
  4713   starfun_mult_CFinite_capprox <-- starfun{C,RC}_mult_CFinite_capprox
  4714   starfun_add_capprox <-- starfun{C,RC}_add_capprox
  4715   starfun_add_approx <-- starfunCR_add_approx
  4716   starfun_inverse_inverse <-- starfunC_inverse_inverse
  4717   starfun_divide <-- starfun{C,CR,RC}_divide
  4718   starfun_n <-- starfun{Nat,C}_n
  4719   starfun_n_mult <-- starfun{Nat,C}_n_mult
  4720   starfun_n_add <-- starfun{Nat,C}_n_add
  4721   starfun_n_add_minus <-- starfunNat_n_add_minus
  4722   starfun_n_const_fun <-- starfun{Nat,C}_n_const_fun
  4723   starfun_n_minus <-- starfun{Nat,C}_n_minus
  4724   starfun_n_eq <-- starfun{Nat,C}_n_eq
  4725 
  4726   star_n_add <-- {hypreal,hypnat,hcomplex}_add
  4727   star_n_minus <-- {hypreal,hcomplex}_minus
  4728   star_n_diff <-- {hypreal,hcomplex}_diff
  4729   star_n_mult <-- {hypreal,hcomplex}_mult
  4730   star_n_inverse <-- {hypreal,hcomplex}_inverse
  4731   star_n_le <-- {hypreal,hypnat}_le
  4732   star_n_less <-- {hypreal,hypnat}_less
  4733   star_n_zero_num <-- {hypreal,hypnat,hcomplex}_zero_num
  4734   star_n_one_num <-- {hypreal,hypnat,hcomplex}_one_num
  4735   star_n_abs <-- hypreal_hrabs
  4736   star_n_divide <-- hcomplex_divide
  4737 
  4738   star_of_add <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_add
  4739   star_of_minus <-- {hypreal_of_real,hcomplex_of_complex}_minus
  4740   star_of_diff <-- hypreal_of_real_diff
  4741   star_of_mult <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_mult
  4742   star_of_one <-- {hypreal_of_real,hcomplex_of_complex}_one
  4743   star_of_zero <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_zero
  4744   star_of_le <-- {hypreal_of_real,hypnat_of_nat}_le_iff
  4745   star_of_less <-- {hypreal_of_real,hypnat_of_nat}_less_iff
  4746   star_of_eq <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_eq_iff
  4747   star_of_inverse <-- {hypreal_of_real,hcomplex_of_complex}_inverse
  4748   star_of_divide <-- {hypreal_of_real,hcomplex_of_complex}_divide
  4749   star_of_of_nat <-- {hypreal_of_real,hcomplex_of_complex}_of_nat
  4750   star_of_of_int <-- {hypreal_of_real,hcomplex_of_complex}_of_int
  4751   star_of_number_of <-- {hypreal,hcomplex}_number_of
  4752   star_of_number_less <-- number_of_less_hypreal_of_real_iff
  4753   star_of_number_le <-- number_of_le_hypreal_of_real_iff
  4754   star_of_eq_number <-- hypreal_of_real_eq_number_of_iff
  4755   star_of_less_number <-- hypreal_of_real_less_number_of_iff
  4756   star_of_le_number <-- hypreal_of_real_le_number_of_iff
  4757   star_of_power <-- hypreal_of_real_power
  4758   star_of_eq_0 <-- hcomplex_of_complex_zero_iff
  4759 
  4760 * Hyperreal: new method "transfer" that implements the transfer
  4761 principle of nonstandard analysis. With a subgoal that mentions
  4762 nonstandard types like "'a star", the command "apply transfer"
  4763 replaces it with an equivalent one that mentions only standard types.
  4764 To be successful, all free variables must have standard types; non-
  4765 standard variables must have explicit universal quantifiers.
  4766 
  4767 * Hyperreal: A theory of Taylor series.
  4768 
  4769 
  4770 *** HOLCF ***
  4771 
  4772 * Discontinued special version of 'constdefs' (which used to support
  4773 continuous functions) in favor of the general Pure one with full
  4774 type-inference.
  4775 
  4776 * New simplification procedure for solving continuity conditions; it
  4777 is much faster on terms with many nested lambda abstractions (cubic
  4778 instead of exponential time).
  4779 
  4780 * New syntax for domain package: selector names are now optional.
  4781 Parentheses should be omitted unless argument is lazy, for example:
  4782 
  4783   domain 'a stream = cons "'a" (lazy "'a stream")
  4784 
  4785 * New command 'fixrec' for defining recursive functions with pattern
  4786 matching; defining multiple functions with mutual recursion is also
  4787 supported.  Patterns may include the constants cpair, spair, up, sinl,
  4788 sinr, or any data constructor defined by the domain package. The given
  4789 equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for
  4790 syntax and examples.
  4791 
  4792 * New commands 'cpodef' and 'pcpodef' for defining predicate subtypes
  4793 of cpo and pcpo types. Syntax is exactly like the 'typedef' command,
  4794 but the proof obligation additionally includes an admissibility
  4795 requirement. The packages generate instances of class cpo or pcpo,
  4796 with continuity and strictness theorems for Rep and Abs.
  4797 
  4798 * HOLCF: Many theorems have been renamed according to a more standard naming
  4799 scheme (INCOMPATIBILITY):
  4800 
  4801   foo_inject:  "foo$x = foo$y ==> x = y"
  4802   foo_eq:      "(foo$x = foo$y) = (x = y)"
  4803   foo_less:    "(foo$x << foo$y) = (x << y)"
  4804   foo_strict:  "foo$UU = UU"
  4805   foo_defined: "... ==> foo$x ~= UU"
  4806   foo_defined_iff: "(foo$x = UU) = (x = UU)"
  4807 
  4808 
  4809 *** ZF ***
  4810 
  4811 * ZF/ex: theories Group and Ring provide examples in abstract algebra,
  4812 including the First Isomorphism Theorem (on quotienting by the kernel
  4813 of a homomorphism).
  4814 
  4815 * ZF/Simplifier: install second copy of type solver that actually
  4816 makes use of TC rules declared to Isar proof contexts (or locales);
  4817 the old version is still required for ML proof scripts.
  4818 
  4819 
  4820 *** Cube ***
  4821 
  4822 * Converted to Isar theory format; use locales instead of axiomatic
  4823 theories.
  4824 
  4825 
  4826 *** ML ***
  4827 
  4828 * Pure/library.ML: added ##>, ##>>, #>> -- higher-order counterparts
  4829 for ||>, ||>>, |>>,
  4830 
  4831 * Pure/library.ML no longer defines its own option datatype, but uses
  4832 that of the SML basis, which has constructors NONE and SOME instead of
  4833 None and Some, as well as exception Option.Option instead of OPTION.
  4834 The functions the, if_none, is_some, is_none have been adapted
  4835 accordingly, while Option.map replaces apsome.
  4836 
  4837 * Pure/library.ML: the exception LIST has been given up in favour of
  4838 the standard exceptions Empty and Subscript, as well as
  4839 Library.UnequalLengths.  Function like Library.hd and Library.tl are
  4840 superceded by the standard hd and tl functions etc.
  4841 
  4842 A number of basic list functions are no longer exported to the ML
  4843 toplevel, as they are variants of predefined functions.  The following
  4844 suggests how one can translate existing code:
  4845 
  4846     rev_append xs ys = List.revAppend (xs, ys)
  4847     nth_elem (i, xs) = List.nth (xs, i)
  4848     last_elem xs = List.last xs
  4849     flat xss = List.concat xss
  4850     seq fs = List.app fs
  4851     partition P xs = List.partition P xs
  4852     mapfilter f xs = List.mapPartial f xs
  4853 
  4854 * Pure/library.ML: several combinators for linear functional
  4855 transformations, notably reverse application and composition:
  4856 
  4857   x |> f                f #> g
  4858   (x, y) |-> f          f #-> g
  4859 
  4860 * Pure/library.ML: introduced/changed precedence of infix operators:
  4861 
  4862   infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
  4863   infix 2 ?;
  4864   infix 3 o oo ooo oooo;
  4865   infix 4 ~~ upto downto;
  4866 
  4867 Maybe INCOMPATIBILITY when any of those is used in conjunction with other
  4868 infix operators.
  4869 
  4870 * Pure/library.ML: natural list combinators fold, fold_rev, and
  4871 fold_map support linear functional transformations and nesting.  For
  4872 example:
  4873 
  4874   fold f [x1, ..., xN] y =
  4875     y |> f x1 |> ... |> f xN
  4876 
  4877   (fold o fold) f [xs1, ..., xsN] y =
  4878     y |> fold f xs1 |> ... |> fold f xsN
  4879 
  4880   fold f [x1, ..., xN] =
  4881     f x1 #> ... #> f xN
  4882 
  4883   (fold o fold) f [xs1, ..., xsN] =
  4884     fold f xs1 #> ... #> fold f xsN
  4885 
  4886 * Pure/library.ML: the following selectors on type 'a option are
  4887 available:
  4888 
  4889   the:               'a option -> 'a  (*partial*)
  4890   these:             'a option -> 'a  where 'a = 'b list
  4891   the_default: 'a -> 'a option -> 'a
  4892   the_list:          'a option -> 'a list
  4893 
  4894 * Pure/General: structure AList (cf. Pure/General/alist.ML) provides
  4895 basic operations for association lists, following natural argument
  4896 order; moreover the explicit equality predicate passed here avoids
  4897 potentially expensive polymorphic runtime equality checks.
  4898 The old functions may be expressed as follows:
  4899 
  4900   assoc = uncurry (AList.lookup (op =))
  4901   assocs = these oo AList.lookup (op =)
  4902   overwrite = uncurry (AList.update (op =)) o swap
  4903 
  4904 * Pure/General: structure AList (cf. Pure/General/alist.ML) provides
  4905 
  4906   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
  4907   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
  4908 
  4909 replacing make_keylist and keyfilter (occassionally used)
  4910 Naive rewrites:
  4911 
  4912   make_keylist = AList.make
  4913   keyfilter = AList.find (op =)
  4914 
  4915 * eq_fst and eq_snd now take explicit equality parameter, thus
  4916   avoiding eqtypes. Naive rewrites:
  4917 
  4918     eq_fst = eq_fst (op =)
  4919     eq_snd = eq_snd (op =)
  4920 
  4921 * Removed deprecated apl and apr (rarely used).
  4922   Naive rewrites:
  4923 
  4924     apl (n, op) =>>= curry op n
  4925     apr (op, m) =>>= fn n => op (n, m)
  4926 
  4927 * Pure/General: structure OrdList (cf. Pure/General/ord_list.ML)
  4928 provides a reasonably efficient light-weight implementation of sets as
  4929 lists.
  4930 
  4931 * Pure/General: generic tables (cf. Pure/General/table.ML) provide a
  4932 few new operations; existing lookup and update are now curried to
  4933 follow natural argument order (for use with fold etc.);
  4934 INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort.
  4935 
  4936 * Pure/General: output via the Isabelle channels of
  4937 writeln/warning/error etc. is now passed through Output.output, with a
  4938 hook for arbitrary transformations depending on the print_mode
  4939 (cf. Output.add_mode -- the first active mode that provides a output
  4940 function wins).  Already formatted output may be embedded into further
  4941 text via Output.raw; the result of Pretty.string_of/str_of and derived
  4942 functions (string_of_term/cterm/thm etc.) is already marked raw to
  4943 accommodate easy composition of diagnostic messages etc.  Programmers
  4944 rarely need to care about Output.output or Output.raw at all, with
  4945 some notable exceptions: Output.output is required when bypassing the
  4946 standard channels (writeln etc.), or in token translations to produce
  4947 properly formatted results; Output.raw is required when capturing
  4948 already output material that will eventually be presented to the user
  4949 a second time.  For the default print mode, both Output.output and
  4950 Output.raw have no effect.
  4951 
  4952 * Pure/General: Output.time_accumulator NAME creates an operator ('a
  4953 -> 'b) -> 'a -> 'b to measure runtime and count invocations; the
  4954 cumulative results are displayed at the end of a batch session.
  4955 
  4956 * Pure/General: File.sysify_path and File.quote_sysify path have been
  4957 replaced by File.platform_path and File.shell_path (with appropriate
  4958 hooks).  This provides a clean interface for unusual systems where the
  4959 internal and external process view of file names are different.
  4960 
  4961 * Pure: more efficient orders for basic syntactic entities: added
  4962 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
  4963 and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is
  4964 NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast
  4965 orders now -- potential INCOMPATIBILITY for code that depends on a
  4966 particular order for Symtab.keys, Symtab.dest, etc. (consider using
  4967 Library.sort_strings on result).
  4968 
  4969 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
  4970 fold_types traverse types/terms from left to right, observing natural
  4971 argument order.  Supercedes previous foldl_XXX versions, add_frees,
  4972 add_vars etc. have been adapted as well: INCOMPATIBILITY.
  4973 
  4974 * Pure: name spaces have been refined, with significant changes of the
  4975 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
  4976 to extern(_table).  The plain name entry path is superceded by a
  4977 general 'naming' context, which also includes the 'policy' to produce
  4978 a fully qualified name and external accesses of a fully qualified
  4979 name; NameSpace.extend is superceded by context dependent
  4980 Sign.declare_name.  Several theory and proof context operations modify
  4981 the naming context.  Especially note Theory.restore_naming and
  4982 ProofContext.restore_naming to get back to a sane state; note that
  4983 Theory.add_path is no longer sufficient to recover from
  4984 Theory.absolute_path in particular.
  4985 
  4986 * Pure: new flags short_names (default false) and unique_names
  4987 (default true) for controlling output of qualified names.  If
  4988 short_names is set, names are printed unqualified.  If unique_names is
  4989 reset, the name prefix is reduced to the minimum required to achieve
  4990 the original result when interning again, even if there is an overlap
  4991 with earlier declarations.
  4992 
  4993 * Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is
  4994 now 'extend', and 'merge' gets an additional Pretty.pp argument
  4995 (useful for printing error messages).  INCOMPATIBILITY.
  4996 
  4997 * Pure: major reorganization of the theory context.  Type Sign.sg and
  4998 Theory.theory are now identified, referring to the universal
  4999 Context.theory (see Pure/context.ML).  Actual signature and theory
  5000 content is managed as theory data.  The old code and interfaces were
  5001 spread over many files and structures; the new arrangement introduces
  5002 considerable INCOMPATIBILITY to gain more clarity:
  5003 
  5004   Context -- theory management operations (name, identity, inclusion,
  5005     parents, ancestors, merge, etc.), plus generic theory data;
  5006 
  5007   Sign -- logical signature and syntax operations (declaring consts,
  5008     types, etc.), plus certify/read for common entities;
  5009 
  5010   Theory -- logical theory operations (stating axioms, definitions,
  5011     oracles), plus a copy of logical signature operations (consts,
  5012     types, etc.); also a few basic management operations (Theory.copy,
  5013     Theory.merge, etc.)
  5014 
  5015 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm
  5016 etc.) as well as the sign field in Thm.rep_thm etc. have been retained
  5017 for convenience -- they merely return the theory.
  5018 
  5019 * Pure: type Type.tsig is superceded by theory in most interfaces.
  5020 
  5021 * Pure: the Isar proof context type is already defined early in Pure
  5022 as Context.proof (note that ProofContext.context and Proof.context are
  5023 aliases, where the latter is the preferred name).  This enables other
  5024 Isabelle components to refer to that type even before Isar is present.
  5025 
  5026 * Pure/sign/theory: discontinued named name spaces (i.e. classK,
  5027 typeK, constK, axiomK, oracleK), but provide explicit operations for
  5028 any of these kinds.  For example, Sign.intern typeK is now
  5029 Sign.intern_type, Theory.hide_space Sign.typeK is now
  5030 Theory.hide_types.  Also note that former
  5031 Theory.hide_classes/types/consts are now
  5032 Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions
  5033 internalize their arguments!  INCOMPATIBILITY.
  5034 
  5035 * Pure: get_thm interface (of PureThy and ProofContext) expects
  5036 datatype thmref (with constructors Name and NameSelection) instead of
  5037 plain string -- INCOMPATIBILITY;
  5038 
  5039 * Pure: cases produced by proof methods specify options, where NONE
  5040 means to remove case bindings -- INCOMPATIBILITY in
  5041 (RAW_)METHOD_CASES.
  5042 
  5043 * Pure: the following operations retrieve axioms or theorems from a
  5044 theory node or theory hierarchy, respectively:
  5045 
  5046   Theory.axioms_of: theory -> (string * term) list
  5047   Theory.all_axioms_of: theory -> (string * term) list
  5048   PureThy.thms_of: theory -> (string * thm) list
  5049   PureThy.all_thms_of: theory -> (string * thm) list
  5050 
  5051 * Pure: print_tac now outputs the goal through the trace channel.
  5052 
  5053 * Isar toplevel: improved diagnostics, mostly for Poly/ML only.
  5054 Reference Toplevel.debug (default false) controls detailed printing
  5055 and tracing of low-level exceptions; Toplevel.profiling (default 0)
  5056 controls execution profiling -- set to 1 for time and 2 for space
  5057 (both increase the runtime).
  5058 
  5059 * Isar session: The initial use of ROOT.ML is now always timed,
  5060 i.e. the log will show the actual process times, in contrast to the
  5061 elapsed wall-clock time that the outer shell wrapper produces.
  5062 
  5063 * Simplifier: improved handling of bound variables (nameless
  5064 representation, avoid allocating new strings).  Simprocs that invoke
  5065 the Simplifier recursively should use Simplifier.inherit_bounds to
  5066 avoid local name clashes.  Failure to do so produces warnings
  5067 "Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds
  5068 for further details.
  5069 
  5070 * ML functions legacy_bindings and use_legacy_bindings produce ML fact
  5071 bindings for all theorems stored within a given theory; this may help
  5072 in porting non-Isar theories to Isar ones, while keeping ML proof
  5073 scripts for the time being.
  5074 
  5075 * ML operator HTML.with_charset specifies the charset begin used for
  5076 generated HTML files.  For example:
  5077 
  5078   HTML.with_charset "utf-8" use_thy "Hebrew";
  5079   HTML.with_charset "utf-8" use_thy "Chinese";
  5080 
  5081 
  5082 *** System ***
  5083 
  5084 * Allow symlinks to all proper Isabelle executables (Isabelle,
  5085 isabelle, isatool etc.).
  5086 
  5087 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for
  5088 isatool doc, isatool mkdir, display_drafts etc.).
  5089 
  5090 * isatool usedir: option -f allows specification of the ML file to be
  5091 used by Isabelle; default is ROOT.ML.
  5092 
  5093 * New isatool version outputs the version identifier of the Isabelle
  5094 distribution being used.
  5095 
  5096 * HOL: new isatool dimacs2hol converts files in DIMACS CNF format
  5097 (containing Boolean satisfiability problems) into Isabelle/HOL
  5098 theories.
  5099 
  5100 
  5101 
  5102 New in Isabelle2004 (April 2004)
  5103 --------------------------------
  5104 
  5105 *** General ***
  5106 
  5107 * Provers/order.ML:  new efficient reasoner for partial and linear orders.
  5108   Replaces linorder.ML.
  5109 
  5110 * Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic
  5111   (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler
  5112   (\<a>...\<z>), are now considered normal letters, and can therefore
  5113   be used anywhere where an ASCII letter (a...zA...Z) has until
  5114   now. COMPATIBILITY: This obviously changes the parsing of some
  5115   terms, especially where a symbol has been used as a binder, say
  5116   '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
  5117   as an identifier.  Fix it by inserting a space around former
  5118   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
  5119   existing theory and ML files.
  5120 
  5121 * Pure: Macintosh and Windows line-breaks are now allowed in theory files.
  5122 
  5123 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now
  5124   allowed in identifiers. Similar to Greek letters \<^isub> is now considered
  5125   a normal (but invisible) letter. For multiple letter subscripts repeat
  5126   \<^isub> like this: x\<^isub>1\<^isub>2.
  5127 
  5128 * Pure: There are now sub-/superscripts that can span more than one
  5129   character. Text between \<^bsub> and \<^esub> is set in subscript in
  5130   ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
  5131   superscript. The new control characters are not identifier parts.
  5132 
  5133 * Pure: Control-symbols of the form \<^raw:...> will literally print the
  5134   content of "..." to the latex file instead of \isacntrl... . The "..."
  5135   may consist of any printable characters excluding the end bracket >.
  5136 
  5137 * Pure: Using new Isar command "finalconsts" (or the ML functions
  5138   Theory.add_finals or Theory.add_finals_i) it is now possible to
  5139   declare constants "final", which prevents their being given a definition
  5140   later.  It is useful for constants whose behaviour is fixed axiomatically
  5141   rather than definitionally, such as the meta-logic connectives.
  5142 
  5143 * Pure: 'instance' now handles general arities with general sorts
  5144   (i.e. intersections of classes),
  5145 
  5146 * Presentation: generated HTML now uses a CSS style sheet to make layout
  5147   (somewhat) independent of content. It is copied from lib/html/isabelle.css.
  5148   It can be changed to alter the colors/layout of generated pages.
  5149 
  5150 
  5151 *** Isar ***
  5152 
  5153 * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
  5154   cut_tac, subgoal_tac and thin_tac:
  5155   - Now understand static (Isar) contexts.  As a consequence, users of Isar
  5156     locales are no longer forced to write Isar proof scripts.
  5157     For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
  5158     emulations.
  5159   - INCOMPATIBILITY: names of variables to be instantiated may no
  5160     longer be enclosed in quotes.  Instead, precede variable name with `?'.
  5161     This is consistent with the instantiation attribute "where".
  5162 
  5163 * Attributes "where" and "of":
  5164   - Now take type variables of instantiated theorem into account when reading
  5165     the instantiation string.  This fixes a bug that caused instantiated
  5166     theorems to have too special types in some circumstances.
  5167   - "where" permits explicit instantiations of type variables.
  5168 
  5169 * Calculation commands "moreover" and "also" no longer interfere with
  5170   current facts ("this"), admitting arbitrary combinations with "then"
  5171   and derived forms.
  5172 
  5173 * Locales:
  5174   - Goal statements involving the context element "includes" no longer
  5175     generate theorems with internal delta predicates (those ending on
  5176     "_axioms") in the premise.
  5177     Resolve particular premise with <locale>.intro to obtain old form.
  5178   - Fixed bug in type inference ("unify_frozen") that prevented mix of target
  5179     specification and "includes" elements in goal statement.
  5180   - Rule sets <locale>.intro and <locale>.axioms no longer declared as
  5181     [intro?] and [elim?] (respectively) by default.
  5182   - Experimental command for instantiation of locales in proof contexts:
  5183         instantiate <label>[<attrs>]: <loc>
  5184     Instantiates locale <loc> and adds all its theorems to the current context
  5185     taking into account their attributes.  Label and attrs are optional
  5186     modifiers, like in theorem declarations.  If present, names of
  5187     instantiated theorems are qualified with <label>, and the attributes
  5188     <attrs> are applied after any attributes these theorems might have already.
  5189       If the locale has assumptions, a chained fact of the form
  5190     "<loc> t1 ... tn" is expected from which instantiations of the parameters
  5191     are derived.  The command does not support old-style locales declared
  5192     with "locale (open)".
  5193       A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
  5194 
  5195 * HOL: Tactic emulation methods induct_tac and case_tac understand static
  5196   (Isar) contexts.
  5197 
  5198 
  5199 *** HOL ***
  5200 
  5201 * Proof import: new image HOL4 contains the imported library from
  5202   the HOL4 system with about 2500 theorems. It is imported by
  5203   replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
  5204   can be used like any other Isabelle image.  See
  5205   HOL/Import/HOL/README for more information.
  5206 
  5207 * Simplifier:
  5208   - Much improved handling of linear and partial orders.
  5209     Reasoners for linear and partial orders are set up for type classes
  5210     "linorder" and "order" respectively, and are added to the default simpset
  5211     as solvers.  This means that the simplifier can build transitivity chains
  5212     to solve goals from the assumptions.
  5213   - INCOMPATIBILITY: old proofs break occasionally.  Typically, applications
  5214     of blast or auto after simplification become unnecessary because the goal
  5215     is solved by simplification already.
  5216 
  5217 * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws,
  5218     all proved in axiomatic type classes for semirings, rings and fields.
  5219 
  5220 * Numerics:
  5221   - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are
  5222     now formalized using the Ring_and_Field theory mentioned above.
  5223   - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently
  5224     than before, because now they are set up once in a generic manner.
  5225   - INCOMPATIBILITY: many type-specific arithmetic laws have gone.
  5226     Look for the general versions in Ring_and_Field (and Power if they concern
  5227     exponentiation).
  5228 
  5229 * Type "rat" of the rational numbers is now available in HOL-Complex.
  5230 
  5231 * Records:
  5232   - Record types are now by default printed with their type abbreviation
  5233     instead of the list of all field types. This can be configured via
  5234     the reference "print_record_type_abbr".
  5235   - Simproc "record_upd_simproc" for simplification of multiple updates added
  5236     (not enabled by default).
  5237   - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp.
  5238     EX x. x = sel r to True (not enabled by default).
  5239   - Tactic "record_split_simp_tac" to split and simplify records added.
  5240 
  5241 * 'specification' command added, allowing for definition by
  5242   specification.  There is also an 'ax_specification' command that
  5243   introduces the new constants axiomatically.
  5244 
  5245 * arith(_tac) is now able to generate counterexamples for reals as well.
  5246 
  5247 * HOL-Algebra: new locale "ring" for non-commutative rings.
  5248 
  5249 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
  5250   definitions, thanks to Sava Krsti\'{c} and John Matthews.
  5251 
  5252 * HOL-Matrix: a first theory for matrices in HOL with an application of
  5253   matrix theory to linear programming.
  5254 
  5255 * Unions and Intersections:
  5256   The latex output syntax of UN and INT has been changed
  5257   from "\Union x \in A. B" to "\Union_{x \in A} B"
  5258   i.e. the index formulae has become a subscript.
  5259   Similarly for "\Union x. B", and for \Inter instead of \Union.
  5260 
  5261 * Unions and Intersections over Intervals:
  5262   There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is
  5263   also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A"
  5264   like in normal math, and corresponding versions for < and for intersection.
  5265 
  5266 * HOL/List: Ordering "lexico" is renamed "lenlex" and the standard
  5267   lexicographic dictonary ordering has been added as "lexord".
  5268 
  5269 * ML: the legacy theory structures Int and List have been removed. They had
  5270   conflicted with ML Basis Library structures having the same names.
  5271 
  5272 * 'refute' command added to search for (finite) countermodels.  Only works
  5273   for a fragment of HOL.  The installation of an external SAT solver is
  5274   highly recommended.  See "HOL/Refute.thy" for details.
  5275 
  5276 * 'quickcheck' command: Allows to find counterexamples by evaluating
  5277   formulae under an assignment of free variables to random values.
  5278   In contrast to 'refute', it can deal with inductive datatypes,
  5279   but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy"
  5280   for examples.
  5281 
  5282 
  5283 *** HOLCF ***
  5284 
  5285 * Streams now come with concatenation and are part of the HOLCF image
  5286 
  5287 
  5288 
  5289 New in Isabelle2003 (May 2003)
  5290 ------------------------------
  5291 
  5292 *** General ***
  5293 
  5294 * Provers/simplifier:
  5295 
  5296   - Completely reimplemented method simp (ML: Asm_full_simp_tac):
  5297     Assumptions are now subject to complete mutual simplification,
  5298     not just from left to right. The simplifier now preserves
  5299     the order of assumptions.
  5300 
  5301     Potential INCOMPATIBILITY:
  5302 
  5303     -- simp sometimes diverges where the old version did
  5304        not, e.g. invoking simp on the goal
  5305 
  5306         [| P (f x); y = x; f x = f y |] ==> Q
  5307 
  5308        now gives rise to the infinite reduction sequence
  5309 
  5310         P(f x) --(f x = f y)--> P(f y) --(y = x)--> P(f x) --(f x = f y)--> ...
  5311 
  5312        Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this
  5313        kind of problem.
  5314 
  5315     -- Tactics combining classical reasoner and simplification (such as auto)
  5316        are also affected by this change, because many of them rely on
  5317        simp. They may sometimes diverge as well or yield a different numbers
  5318        of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto
  5319        in case of problems. Sometimes subsequent calls to the classical
  5320        reasoner will fail because a preceeding call to the simplifier too
  5321        eagerly simplified the goal, e.g. deleted redundant premises.
  5322 
  5323   - The simplifier trace now shows the names of the applied rewrite rules
  5324 
  5325   - You can limit the number of recursive invocations of the simplifier
  5326     during conditional rewriting (where the simplifie tries to solve the
  5327     conditions before applying the rewrite rule):
  5328     ML "simp_depth_limit := n"
  5329     where n is an integer. Thus you can force termination where previously
  5330     the simplifier would diverge.
  5331 
  5332   - Accepts free variables as head terms in congruence rules.  Useful in Isar.
  5333 
  5334   - No longer aborts on failed congruence proof.  Instead, the
  5335     congruence is ignored.
  5336 
  5337 * Pure: New generic framework for extracting programs from constructive
  5338   proofs. See HOL/Extraction.thy for an example instantiation, as well
  5339   as HOL/Extraction for some case studies.
  5340 
  5341 * Pure: The main goal of the proof state is no longer shown by default, only
  5342 the subgoals. This behaviour is controlled by a new flag.
  5343    PG menu: Isabelle/Isar -> Settings -> Show Main Goal
  5344 (ML: Proof.show_main_goal).
  5345 
  5346 * Pure: You can find all matching introduction rules for subgoal 1, i.e. all
  5347 rules whose conclusion matches subgoal 1:
  5348       PG menu: Isabelle/Isar -> Show me -> matching rules
  5349 The rules are ordered by how closely they match the subgoal.
  5350 In particular, rules that solve a subgoal outright are displayed first
  5351 (or rather last, the way they are printed).
  5352 (ML: ProofGeneral.print_intros())
  5353 
  5354 * Pure: New flag trace_unify_fail causes unification to print
  5355 diagnostic information (PG: in trace buffer) when it fails. This is
  5356 useful for figuring out why single step proofs like rule, erule or
  5357 assumption failed.
  5358 
  5359 * Pure: Locale specifications now produce predicate definitions
  5360 according to the body of text (covering assumptions modulo local
  5361 definitions); predicate "loc_axioms" covers newly introduced text,
  5362 while "loc" is cumulative wrt. all included locale expressions; the
  5363 latter view is presented only on export into the global theory
  5364 context; potential INCOMPATIBILITY, use "(open)" option to fall back
  5365 on the old view without predicates;
  5366 
  5367 * Pure: predefined locales "var" and "struct" are useful for sharing
  5368 parameters (as in CASL, for example); just specify something like
  5369 ``var x + var y + struct M'' as import;
  5370 
  5371 * Pure: improved thms_containing: proper indexing of facts instead of
  5372 raw theorems; check validity of results wrt. current name space;
  5373 include local facts of proof configuration (also covers active
  5374 locales), cover fixed variables in index; may use "_" in term
  5375 specification; an optional limit for the number of printed facts may
  5376 be given (the default is 40);
  5377 
  5378 * Pure: disallow duplicate fact bindings within new-style theory files
  5379 (batch-mode only);
  5380 
  5381 * Provers: improved induct method: assumptions introduced by case
  5382 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
  5383 the goal statement); "foo" still refers to all facts collectively;
  5384 
  5385 * Provers: the function blast.overloaded has been removed: all constants
  5386 are regarded as potentially overloaded, which improves robustness in exchange
  5387 for slight decrease in efficiency;
  5388 
  5389 * Provers/linorder: New generic prover for transitivity reasoning over
  5390 linear orders.  Note: this prover is not efficient!
  5391 
  5392 * Isar: preview of problems to finish 'show' now produce an error
  5393 rather than just a warning (in interactive mode);
  5394 
  5395 
  5396 *** HOL ***
  5397 
  5398 * arith(_tac)
  5399 
  5400  - Produces a counter example if it cannot prove a goal.
  5401    Note that the counter example may be spurious if the goal is not a formula
  5402    of quantifier-free linear arithmetic.
  5403    In ProofGeneral the counter example appears in the trace buffer.
  5404 
  5405  - Knows about div k and mod k where k is a numeral of type nat or int.
  5406 
  5407  - Calls full Presburger arithmetic (by Amine Chaieb) if quantifier-free
  5408    linear arithmetic fails. This takes account of quantifiers and divisibility.
  5409    Presburger arithmetic can also be called explicitly via presburger(_tac).
  5410 
  5411 * simp's arithmetic capabilities have been enhanced a bit: it now
  5412 takes ~= in premises into account (by performing a case split);
  5413 
  5414 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands
  5415 are distributed over a sum of terms;
  5416 
  5417 * New tactic "trans_tac" and method "trans" instantiate
  5418 Provers/linorder.ML for axclasses "order" and "linorder" (predicates
  5419 "<=", "<" and "=").
  5420 
  5421 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main
  5422 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
  5423 
  5424 * 'typedef' command has new option "open" to suppress the set
  5425 definition;
  5426 
  5427 * functions Min and Max on finite sets have been introduced (theory
  5428 Finite_Set);
  5429 
  5430 * attribute [symmetric] now works for relations as well; it turns
  5431 (x,y) : R^-1 into (y,x) : R, and vice versa;
  5432 
  5433 * induct over a !!-quantified statement (say !!x1..xn):
  5434   each "case" automatically performs "fix x1 .. xn" with exactly those names.
  5435 
  5436 * Map: `empty' is no longer a constant but a syntactic abbreviation for
  5437 %x. None. Warning: empty_def now refers to the previously hidden definition
  5438 of the empty set.
  5439 
  5440 * Algebra: formalization of classical algebra.  Intended as base for
  5441 any algebraic development in Isabelle.  Currently covers group theory
  5442 (up to Sylow's theorem) and ring theory (Universal Property of
  5443 Univariate Polynomials).  Contributions welcome;
  5444 
  5445 * GroupTheory: deleted, since its material has been moved to Algebra;
  5446 
  5447 * Complex: new directory of the complex numbers with numeric constants,
  5448 nonstandard complex numbers, and some complex analysis, standard and
  5449 nonstandard (Jacques Fleuriot);
  5450 
  5451 * HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal;
  5452 
  5453 * Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques
  5454 Fleuriot);
  5455 
  5456 * Real/HahnBanach: updated and adapted to locales;
  5457 
  5458 * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad,
  5459 Gray and Kramer);
  5460 
  5461 * UNITY: added the Meier-Sanders theory of progress sets;
  5462 
  5463 * MicroJava: bytecode verifier and lightweight bytecode verifier
  5464 as abstract algorithms, instantiated to the JVM;
  5465 
  5466 * Bali: Java source language formalization. Type system, operational
  5467 semantics, axiomatic semantics. Supported language features:
  5468 classes, interfaces, objects,virtual methods, static methods,
  5469 static/instance fields, arrays, access modifiers, definite
  5470 assignment, exceptions.
  5471 
  5472 
  5473 *** ZF ***
  5474 
  5475 * ZF/Constructible: consistency proof for AC (Gdel's constructible
  5476 universe, etc.);
  5477 
  5478 * Main ZF: virtually all theories converted to new-style format;
  5479 
  5480 
  5481 *** ML ***
  5482 
  5483 * Pure: Tactic.prove provides sane interface for internal proofs;
  5484 omits the infamous "standard" operation, so this is more appropriate
  5485 than prove_goalw_cterm in many situations (e.g. in simprocs);
  5486 
  5487 * Pure: improved error reporting of simprocs;
  5488 
  5489 * Provers: Simplifier.simproc(_i) provides sane interface for setting
  5490 up simprocs;
  5491 
  5492 
  5493 *** Document preparation ***
  5494 
  5495 * uses \par instead of \\ for line breaks in theory text. This may
  5496 shift some page breaks in large documents. To get the old behaviour
  5497 use \renewcommand{\isanewline}{\mbox{}\\\mbox{}} in root.tex.
  5498 
  5499 * minimized dependencies of isabelle.sty and isabellesym.sty on
  5500 other packages
  5501 
  5502 * \<euro> now needs package babel/greek instead of marvosym (which
  5503 broke \Rightarrow)
  5504 
  5505 * normal size for \<zero>...\<nine> (uses \mathbf instead of
  5506 textcomp package)
  5507 
  5508 
  5509 
  5510 New in Isabelle2002 (March 2002)
  5511 --------------------------------
  5512 
  5513 *** Document preparation ***
  5514 
  5515 * greatly simplified document preparation setup, including more
  5516 graceful interpretation of isatool usedir -i/-d/-D options, and more
  5517 instructive isatool mkdir; users should basically be able to get
  5518 started with "isatool mkdir HOL Test && isatool make"; alternatively,
  5519 users may run a separate document processing stage manually like this:
  5520 "isatool usedir -D output HOL Test && isatool document Test/output";
  5521 
  5522 * theory dependency graph may now be incorporated into documents;
  5523 isatool usedir -g true will produce session_graph.eps/.pdf for use
  5524 with \includegraphics of LaTeX;
  5525 
  5526 * proper spacing of consecutive markup elements, especially text
  5527 blocks after section headings;
  5528 
  5529 * support bold style (for single symbols only), input syntax is like
  5530 this: "\<^bold>\<alpha>" or "\<^bold>A";
  5531 
  5532 * \<bullet> is now output as bold \cdot by default, which looks much
  5533 better in printed text;
  5534 
  5535 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
  5536 note that these symbols are currently unavailable in Proof General /
  5537 X-Symbol; new symbols \<zero>, \<one>, ..., \<nine>, and \<euro>;
  5538 
  5539 * isatool latex no longer depends on changed TEXINPUTS, instead
  5540 isatool document copies the Isabelle style files to the target
  5541 location;
  5542 
  5543 
  5544 *** Isar ***
  5545 
  5546 * Pure/Provers: improved proof by cases and induction;
  5547   - 'case' command admits impromptu naming of parameters (such as
  5548     "case (Suc n)");
  5549   - 'induct' method divinates rule instantiation from the inductive
  5550     claim; no longer requires excessive ?P bindings for proper
  5551     instantiation of cases;
  5552   - 'induct' method properly enumerates all possibilities of set/type
  5553     rules; as a consequence facts may be also passed through *type*
  5554     rules without further ado;
  5555   - 'induct' method now derives symbolic cases from the *rulified*
  5556     rule (before it used to rulify cases stemming from the internal
  5557     atomized version); this means that the context of a non-atomic
  5558     statement becomes is included in the hypothesis, avoiding the
  5559     slightly cumbersome show "PROP ?case" form;
  5560   - 'induct' may now use elim-style induction rules without chaining
  5561     facts, using ``missing'' premises from the goal state; this allows
  5562     rules stemming from inductive sets to be applied in unstructured
  5563     scripts, while still benefitting from proper handling of non-atomic
  5564     statements; NB: major inductive premises need to be put first, all
  5565     the rest of the goal is passed through the induction;
  5566   - 'induct' proper support for mutual induction involving non-atomic
  5567     rule statements (uses the new concept of simultaneous goals, see
  5568     below);
  5569   - append all possible rule selections, but only use the first
  5570     success (no backtracking);
  5571   - removed obsolete "(simplified)" and "(stripped)" options of methods;
  5572   - undeclared rule case names default to numbers 1, 2, 3, ...;
  5573   - added 'print_induct_rules' (covered by help item in recent Proof
  5574     General versions);
  5575   - moved induct/cases attributes to Pure, methods to Provers;
  5576   - generic method setup instantiated for FOL and HOL;
  5577 
  5578 * Pure: support multiple simultaneous goal statements, for example
  5579 "have a: A and b: B" (same for 'theorem' etc.); being a pure
  5580 meta-level mechanism, this acts as if several individual goals had
  5581 been stated separately; in particular common proof methods need to be
  5582 repeated in order to cover all claims; note that a single elimination
  5583 step is *not* sufficient to establish the two conjunctions, so this
  5584 fails:
  5585 
  5586   assume "A & B" then have A and B ..   (*".." fails*)
  5587 
  5588 better use "obtain" in situations as above; alternative refer to
  5589 multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
  5590 
  5591 * Pure: proper integration with ``locales''; unlike the original
  5592 version by Florian Kammller, Isar locales package high-level proof
  5593 contexts rather than raw logical ones (e.g. we admit to include
  5594 attributes everywhere); operations on locales include merge and
  5595 rename; support for implicit arguments (``structures''); simultaneous
  5596 type-inference over imports and text; see also HOL/ex/Locales.thy for
  5597 some examples;
  5598 
  5599 * Pure: the following commands have been ``localized'', supporting a
  5600 target locale specification "(in name)": 'lemma', 'theorem',
  5601 'corollary', 'lemmas', 'theorems', 'declare'; the results will be
  5602 stored both within the locale and at the theory level (exported and
  5603 qualified by the locale name);
  5604 
  5605 * Pure: theory goals may now be specified in ``long'' form, with
  5606 ad-hoc contexts consisting of arbitrary locale elements. for example
  5607 ``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and
  5608 definitions may be given, too); the result is a meta-level rule with
  5609 the context elements being discharged in the obvious way;
  5610 
  5611 * Pure: new proof command 'using' allows to augment currently used
  5612 facts after a goal statement ('using' is syntactically analogous to
  5613 'apply', but acts on the goal's facts only); this allows chained facts
  5614 to be separated into parts given before and after a claim, as in
  5615 ``from a and b have C using d and e <proof>'';
  5616 
  5617 * Pure: renamed "antecedent" case to "rule_context";
  5618 
  5619 * Pure: new 'judgment' command records explicit information about the
  5620 object-logic embedding (used by several tools internally); no longer
  5621 use hard-wired "Trueprop";
  5622 
  5623 * Pure: added 'corollary' command;
  5624 
  5625 * Pure: fixed 'token_translation' command;
  5626 
  5627 * Pure: removed obsolete 'exported' attribute;
  5628 
  5629 * Pure: dummy pattern "_" in is/let is now automatically lifted over
  5630 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
  5631 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
  5632 
  5633 * Pure: method 'atomize' presents local goal premises as object-level
  5634 statements (atomic meta-level propositions); setup controlled via
  5635 rewrite rules declarations of 'atomize' attribute; example
  5636 application: 'induct' method with proper rule statements in improper
  5637 proof *scripts*;
  5638 
  5639 * Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)
  5640 now consider the syntactic context of assumptions, giving a better
  5641 chance to get type-inference of the arguments right (this is
  5642 especially important for locales);
  5643 
  5644 * Pure: "sorry" no longer requires quick_and_dirty in interactive
  5645 mode;
  5646 
  5647 * Pure/obtain: the formal conclusion "thesis", being marked as
  5648 ``internal'', may no longer be reference directly in the text;
  5649 potential INCOMPATIBILITY, may need to use "?thesis" in rare
  5650 situations;
  5651 
  5652 * Pure: generic 'sym' attribute which declares a rule both as pure
  5653 'elim?' and for the 'symmetric' operation;
  5654 
  5655 * Pure: marginal comments ``--'' may now occur just anywhere in the
  5656 text; the fixed correlation with particular command syntax has been
  5657 discontinued;
  5658 
  5659 * Pure: new method 'rules' is particularly well-suited for proof
  5660 search in intuitionistic logic; a bit slower than 'blast' or 'fast',
  5661 but often produces more compact proof terms with less detours;
  5662 
  5663 * Pure/Provers/classical: simplified integration with pure rule
  5664 attributes and methods; the classical "intro?/elim?/dest?"
  5665 declarations coincide with the pure ones; the "rule" method no longer
  5666 includes classically swapped intros; "intro" and "elim" methods no
  5667 longer pick rules from the context; also got rid of ML declarations
  5668 AddXIs/AddXEs/AddXDs; all of this has some potential for
  5669 INCOMPATIBILITY;
  5670 
  5671 * Provers/classical: attribute 'swapped' produces classical inversions
  5672 of introduction rules;
  5673 
  5674 * Provers/simplifier: 'simplified' attribute may refer to explicit
  5675 rules instead of full simplifier context; 'iff' attribute handles
  5676 conditional rules;
  5677 
  5678 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
  5679 
  5680 * HOL: 'recdef' now fails on unfinished automated proofs, use
  5681 "(permissive)" option to recover old behavior;
  5682 
  5683 * HOL: 'inductive' no longer features separate (collective) attributes
  5684 for 'intros' (was found too confusing);
  5685 
  5686 * HOL: properly declared induction rules less_induct and
  5687 wf_induct_rule;
  5688 
  5689 
  5690 *** HOL ***
  5691 
  5692 * HOL: moved over to sane numeral syntax; the new policy is as
  5693 follows:
  5694 
  5695   - 0 and 1 are polymorphic constants, which are defined on any
  5696   numeric type (nat, int, real etc.);
  5697 
  5698   - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based
  5699   binary representation internally;
  5700 
  5701   - type nat has special constructor Suc, and generally prefers Suc 0
  5702   over 1::nat and Suc (Suc 0) over 2::nat;
  5703 
  5704 This change may cause significant problems of INCOMPATIBILITY; here
  5705 are some hints on converting existing sources:
  5706 
  5707   - due to the new "num" token, "-0" and "-1" etc. are now atomic
  5708   entities, so expressions involving "-" (unary or binary minus) need
  5709   to be spaced properly;
  5710 
  5711   - existing occurrences of "1" may need to be constraint "1::nat" or
  5712   even replaced by Suc 0; similar for old "2";
  5713 
  5714   - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";
  5715 
  5716   - remove all special provisions on numerals in proofs;
  5717 
  5718 * HOL: simp rules nat_number expand numerals on nat to Suc/0
  5719 representation (depends on bin_arith_simps in the default context);
  5720 
  5721 * HOL: symbolic syntax for x^2 (numeral 2);
  5722 
  5723 * HOL: the class of all HOL types is now called "type" rather than
  5724 "term"; INCOMPATIBILITY, need to adapt references to this type class
  5725 in axclass/classes, instance/arities, and (usually rare) occurrences
  5726 in typings (of consts etc.); internally the class is called
  5727 "HOL.type", ML programs should refer to HOLogic.typeS;
  5728 
  5729 * HOL/record package improvements:
  5730   - new derived operations "fields" to build a partial record section,
  5731     "extend" to promote a fixed record to a record scheme, and
  5732     "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*
  5733     declared as simp by default;
  5734   - shared operations ("more", "fields", etc.) now need to be always
  5735     qualified) --- potential INCOMPATIBILITY;
  5736   - removed "make_scheme" operations (use "make" with "extend") --
  5737     INCOMPATIBILITY;
  5738   - removed "more" class (simply use "term") -- INCOMPATIBILITY;
  5739   - provides cases/induct rules for use with corresponding Isar
  5740     methods (for concrete records, record schemes, concrete more
  5741     parts, and schematic more parts -- in that order);
  5742   - internal definitions directly based on a light-weight abstract
  5743     theory of product types over typedef rather than datatype;
  5744 
  5745 * HOL: generic code generator for generating executable ML code from
  5746 specifications; specific support for HOL constructs such as inductive
  5747 datatypes and sets, as well as recursive functions; can be invoked
  5748 via 'generate_code' theory section;
  5749 
  5750 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
  5751 
  5752 * HOL: consolidated and renamed several theories.  In particular:
  5753         Ord.thy has been absorbed into HOL.thy
  5754         String.thy has been absorbed into List.thy
  5755 
  5756 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
  5757 (beware of argument permutation!);
  5758 
  5759 * HOL: linorder_less_split superseded by linorder_cases;
  5760 
  5761 * HOL/List: "nodups" renamed to "distinct";
  5762 
  5763 * HOL: added "The" definite description operator; move Hilbert's "Eps"
  5764 to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES:
  5765   - Ex_def has changed, now need to use some_eq_ex
  5766 
  5767 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
  5768 in this (rare) case use:
  5769 
  5770   delSWrapper "split_all_tac"
  5771   addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)
  5772 
  5773 * HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS
  5774 MAY FAIL;
  5775 
  5776 * HOL: introduced f^n = f o ... o f; warning: due to the limits of
  5777 Isabelle's type classes, ^ on functions and relations has too general
  5778 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
  5779 necessary to attach explicit type constraints;
  5780 
  5781 * HOL/Relation: the prefix name of the infix "O" has been changed from
  5782 "comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been
  5783 renamed accordingly (eg "compI" -> "rel_compI").
  5784 
  5785 * HOL: syntax translations now work properly with numerals and records
  5786 expressions;
  5787 
  5788 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
  5789 of "lam" -- INCOMPATIBILITY;
  5790 
  5791 * HOL: got rid of some global declarations (potential INCOMPATIBILITY
  5792 for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
  5793 renamed "Product_Type.unit";
  5794 
  5795 * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
  5796 
  5797 * HOL: removed obsolete theorem "optionE" (use "option.exhaust", or
  5798 the "cases" method);
  5799 
  5800 * HOL/GroupTheory: group theory examples including Sylow's theorem (by
  5801 Florian Kammller);
  5802 
  5803 * HOL/IMP: updated and converted to new-style theory format; several
  5804 parts turned into readable document, with proper Isar proof texts and
  5805 some explanations (by Gerwin Klein);
  5806 
  5807 * HOL-Real: added Complex_Numbers (by Gertrud Bauer);
  5808 
  5809 * HOL-Hyperreal is now a logic image;
  5810 
  5811 
  5812 *** HOLCF ***
  5813 
  5814 * Isar: consts/constdefs supports mixfix syntax for continuous
  5815 operations;
  5816 
  5817 * Isar: domain package adapted to new-style theory format, e.g. see
  5818 HOLCF/ex/Dnat.thy;
  5819 
  5820 * theory Lift: proper use of rep_datatype lift instead of ML hacks --
  5821 potential INCOMPATIBILITY; now use plain induct_tac instead of former
  5822 lift.induct_tac, always use UU instead of Undef;
  5823 
  5824 * HOLCF/IMP: updated and converted to new-style theory;
  5825 
  5826 
  5827 *** ZF ***
  5828 
  5829 * Isar: proper integration of logic-specific tools and packages,
  5830 including theory commands '(co)inductive', '(co)datatype',
  5831 'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',
  5832 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
  5833 
  5834 * theory Main no longer includes AC; for the Axiom of Choice, base
  5835 your theory on Main_ZFC;
  5836 
  5837 * the integer library now covers quotients and remainders, with many
  5838 laws relating division to addition, multiplication, etc.;
  5839 
  5840 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
  5841 typeless version of the formalism;
  5842 
  5843 * ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory
  5844 format;
  5845 
  5846 * ZF/Induct: new directory for examples of inductive definitions,
  5847 including theory Multiset for multiset orderings; converted to
  5848 new-style theory format;
  5849 
  5850 * ZF: many new theorems about lists, ordinals, etc.;
  5851 
  5852 
  5853 *** General ***
  5854 
  5855 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference
  5856 variable proof controls level of detail: 0 = no proofs (only oracle
  5857 dependencies), 1 = lemma dependencies, 2 = compact proof terms; see
  5858 also ref manual for further ML interfaces;
  5859 
  5860 * Pure/axclass: removed obsolete ML interface
  5861 goal_subclass/goal_arity;
  5862 
  5863 * Pure/syntax: new token syntax "num" for plain numerals (without "#"
  5864 of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now
  5865 separate tokens, so expressions involving minus need to be spaced
  5866 properly;
  5867 
  5868 * Pure/syntax: support non-oriented infixes, using keyword "infix"
  5869 rather than "infixl" or "infixr";
  5870 
  5871 * Pure/syntax: concrete syntax for dummy type variables admits genuine
  5872 sort constraint specifications in type inference; e.g. "x::_::foo"
  5873 ensures that the type of "x" is of sort "foo" (but not necessarily a
  5874 type variable);
  5875 
  5876 * Pure/syntax: print modes "type_brackets" and "no_type_brackets"
  5877 control output of nested => (types); the default behavior is
  5878 "type_brackets";
  5879 
  5880 * Pure/syntax: builtin parse translation for "_constify" turns valued
  5881 tokens into AST constants;
  5882 
  5883 * Pure/syntax: prefer later declarations of translations and print
  5884 translation functions; potential INCOMPATIBILITY: need to reverse
  5885 multiple declarations for same syntax element constant;
  5886 
  5887 * Pure/show_hyps reset by default (in accordance to existing Isar
  5888 practice);
  5889 
  5890 * Provers/classical: renamed addaltern to addafter, addSaltern to
  5891 addSafter;
  5892 
  5893 * Provers/clasimp: ``iff'' declarations now handle conditional rules
  5894 as well;
  5895 
  5896 * system: tested support for MacOS X; should be able to get Isabelle +
  5897 Proof General to work in a plain Terminal after installing Poly/ML
  5898 (e.g. from the Isabelle distribution area) and GNU bash alone
  5899 (e.g. from http://www.apple.com); full X11, XEmacs and X-Symbol
  5900 support requires further installations, e.g. from
  5901 http://fink.sourceforge.net/);
  5902 
  5903 * system: support Poly/ML 4.1.1 (able to manage larger heaps);
  5904 
  5905 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead
  5906 of 40 MB), cf. ML_OPTIONS;
  5907 
  5908 * system: Proof General keywords specification is now part of the
  5909 Isabelle distribution (see etc/isar-keywords.el);
  5910 
  5911 * system: support for persistent Proof General sessions (refrain from
  5912 outdating all loaded theories on startup); user may create writable
  5913 logic images like this: ``isabelle -q HOL Test'';
  5914 
  5915 * system: smart selection of Isabelle process versus Isabelle
  5916 interface, accommodates case-insensitive file systems (e.g. HFS+); may
  5917 run both "isabelle" and "Isabelle" even if file names are badly
  5918 damaged (executable inspects the case of the first letter of its own
  5919 name); added separate "isabelle-process" and "isabelle-interface";
  5920 
  5921 * system: refrain from any attempt at filtering input streams; no
  5922 longer support ``8bit'' encoding of old isabelle font, instead proper
  5923 iso-latin characters may now be used; the related isatools
  5924 "symbolinput" and "nonascii" have disappeared as well;
  5925 
  5926 * system: removed old "xterm" interface (the print modes "xterm" and
  5927 "xterm_color" are still available for direct use in a suitable
  5928 terminal);
  5929 
  5930 
  5931 
  5932 New in Isabelle99-2 (February 2001)
  5933 -----------------------------------
  5934 
  5935 *** Overview of INCOMPATIBILITIES ***
  5936 
  5937 * HOL: please note that theories in the Library and elsewhere often use the
  5938 new-style (Isar) format; to refer to their theorems in an ML script you must
  5939 bind them to ML identifers by e.g.      val thm_name = thm "thm_name";
  5940 
  5941 * HOL: inductive package no longer splits induction rule aggressively,
  5942 but only as far as specified by the introductions given; the old
  5943 format may be recovered via ML function complete_split_rule or attribute
  5944 'split_rule (complete)';
  5945 
  5946 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
  5947 gfp_Tarski to gfp_unfold;
  5948 
  5949 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
  5950 
  5951 * HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
  5952 relation); infix "^^" has been renamed "``"; infix "``" has been
  5953 renamed "`"; "univalent" has been renamed "single_valued";
  5954 
  5955 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
  5956 operation;
  5957 
  5958 * HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
  5959 
  5960 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
  5961 
  5962 * Isar/HOL: method 'induct' now handles non-atomic goals; as a
  5963 consequence, it is no longer monotonic wrt. the local goal context
  5964 (which is now passed through the inductive cases);
  5965 
  5966 * Document preparation: renamed standard symbols \<ll> to \<lless> and
  5967 \<gg> to \<ggreater>;
  5968 
  5969 
  5970 *** Document preparation ***
  5971 
  5972 * \isabellestyle{NAME} selects version of Isabelle output (currently
  5973 available: are "it" for near math-mode best-style output, "sl" for
  5974 slanted text style, and "tt" for plain type-writer; if no
  5975 \isabellestyle command is given, output is according to slanted
  5976 type-writer);
  5977 
  5978 * support sub/super scripts (for single symbols only), input syntax is
  5979 like this: "A\<^sup>*" or "A\<^sup>\<star>";
  5980 
  5981 * some more standard symbols; see Appendix A of the system manual for
  5982 the complete list of symbols defined in isabellesym.sty;
  5983 
  5984 * improved isabelle style files; more abstract symbol implementation
  5985 (should now use \isamath{...} and \isatext{...} in custom symbol
  5986 definitions);
  5987 
  5988 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
  5989 state; Note that presentation of goal states does not conform to
  5990 actual human-readable proof documents.  Please do not include goal
  5991 states into document output unless you really know what you are doing!
  5992 
  5993 * proper indentation of antiquoted output with proportional LaTeX
  5994 fonts;
  5995 
  5996 * no_document ML operator temporarily disables LaTeX document
  5997 generation;
  5998 
  5999 * isatool unsymbolize tunes sources for plain ASCII communication;
  6000 
  6001 
  6002 *** Isar ***
  6003 
  6004 * Pure: Isar now suffers initial goal statements to contain unbound
  6005 schematic variables (this does not conform to actual readable proof
  6006 documents, due to unpredictable outcome and non-compositional proof
  6007 checking); users who know what they are doing may use schematic goals
  6008 for Prolog-style synthesis of proven results;
  6009 
  6010 * Pure: assumption method (an implicit finishing) now handles actual
  6011 rules as well;
  6012 
  6013 * Pure: improved 'obtain' --- moved to Pure, insert "that" into
  6014 initial goal, declare "that" only as Pure intro (only for single
  6015 steps); the "that" rule assumption may now be involved in implicit
  6016 finishing, thus ".." becomes a feasible for trivial obtains;
  6017 
  6018 * Pure: default proof step now includes 'intro_classes'; thus trivial
  6019 instance proofs may be performed by "..";
  6020 
  6021 * Pure: ?thesis / ?this / "..." now work for pure meta-level
  6022 statements as well;
  6023 
  6024 * Pure: more robust selection of calculational rules;
  6025 
  6026 * Pure: the builtin notion of 'finished' goal now includes the ==-refl
  6027 rule (as well as the assumption rule);
  6028 
  6029 * Pure: 'thm_deps' command visualizes dependencies of theorems and
  6030 lemmas, using the graph browser tool;
  6031 
  6032 * Pure: predict failure of "show" in interactive mode;
  6033 
  6034 * Pure: 'thms_containing' now takes actual terms as arguments;
  6035 
  6036 * HOL: improved method 'induct' --- now handles non-atomic goals
  6037 (potential INCOMPATIBILITY); tuned error handling;
  6038 
  6039 * HOL: cases and induct rules now provide explicit hints about the
  6040 number of facts to be consumed (0 for "type" and 1 for "set" rules);
  6041 any remaining facts are inserted into the goal verbatim;
  6042 
  6043 * HOL: local contexts (aka cases) may now contain term bindings as
  6044 well; the 'cases' and 'induct' methods new provide a ?case binding for
  6045 the result to be shown in each case;
  6046 
  6047 * HOL: added 'recdef_tc' command;
  6048 
  6049 * isatool convert assists in eliminating legacy ML scripts;
  6050 
  6051 
  6052 *** HOL ***
  6053 
  6054 * HOL/Library: a collection of generic theories to be used together
  6055 with main HOL; the theory loader path already includes this directory
  6056 by default; the following existing theories have been moved here:
  6057 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
  6058 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
  6059 
  6060 * HOL/Unix: "Some aspects of Unix file-system security", a typical
  6061 modelling and verification task performed in Isabelle/HOL +
  6062 Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).
  6063 
  6064 * HOL/Algebra: special summation operator SUM no longer exists, it has
  6065 been replaced by setsum; infix 'assoc' now has priority 50 (like
  6066 'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to
  6067 'domain', this makes the theory consistent with mathematical
  6068 literature;
  6069 
  6070 * HOL basics: added overloaded operations "inverse" and "divide"
  6071 (infix "/"), syntax for generic "abs" operation, generic summation
  6072 operator \<Sum>;
  6073 
  6074 * HOL/typedef: simplified package, provide more useful rules (see also
  6075 HOL/subset.thy);
  6076 
  6077 * HOL/datatype: induction rule for arbitrarily branching datatypes is
  6078 now expressed as a proper nested rule (old-style tactic scripts may
  6079 require atomize_strip_tac to cope with non-atomic premises);
  6080 
  6081 * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
  6082 to "split_conv" (old name still available for compatibility);
  6083 
  6084 * HOL: improved concrete syntax for strings (e.g. allows translation
  6085 rules with string literals);
  6086 
  6087 * HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals
  6088  and Fleuriot's mechanization of analysis, including the transcendental
  6089  functions for the reals;
  6090 
  6091 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
  6092 
  6093 
  6094 *** CTT ***
  6095 
  6096 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
  6097 "lam" is displayed as TWO lambda-symbols
  6098 
  6099 * CTT: theory Main now available, containing everything (that is, Bool
  6100 and Arith);
  6101 
  6102 
  6103 *** General ***
  6104 
  6105 * Pure: the Simplifier has been implemented properly as a derived rule
  6106 outside of the actual kernel (at last!); the overall performance
  6107 penalty in practical applications is about 50%, while reliability of
  6108 the Isabelle inference kernel has been greatly improved;
  6109 
  6110 * print modes "brackets" and "no_brackets" control output of nested =>
  6111 (types) and ==> (props); the default behaviour is "brackets";
  6112 
  6113 * Provers: fast_tac (and friends) now handle actual object-logic rules
  6114 as assumptions as well;
  6115 
  6116 * system: support Poly/ML 4.0;
  6117 
  6118 * system: isatool install handles KDE version 1 or 2;
  6119 
  6120 
  6121 
  6122 New in Isabelle99-1 (October 2000)
  6123 ----------------------------------
  6124 
  6125 *** Overview of INCOMPATIBILITIES ***
  6126 
  6127 * HOL: simplification of natural numbers is much changed; to partly
  6128 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
  6129 issue the following ML commands:
  6130 
  6131   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
  6132   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
  6133 
  6134 * HOL: simplification no longer dives into case-expressions; this is
  6135 controlled by "t.weak_case_cong" for each datatype t;
  6136 
  6137 * HOL: nat_less_induct renamed to less_induct;
  6138 
  6139 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool
  6140 fixsome to patch .thy and .ML sources automatically;
  6141 
  6142   select_equality  -> some_equality
  6143   select_eq_Ex     -> some_eq_ex
  6144   selectI2EX       -> someI2_ex
  6145   selectI2         -> someI2
  6146   selectI          -> someI
  6147   select1_equality -> some1_equality
  6148   Eps_sym_eq       -> some_sym_eq_trivial
  6149   Eps_eq           -> some_eq_trivial
  6150 
  6151 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
  6152 
  6153 * HOL: removed obsolete theorem binding expand_if (refer to split_if
  6154 instead);
  6155 
  6156 * HOL: the recursion equations generated by 'recdef' are now called
  6157 f.simps instead of f.rules;
  6158 
  6159 * HOL: qed_spec_mp now also handles bounded ALL as well;
  6160 
  6161 * HOL: 0 is now overloaded, so the type constraint ":: nat" may
  6162 sometimes be needed;
  6163 
  6164 * HOL: the constant for "f``x" is now "image" rather than "op ``";
  6165 
  6166 * HOL: the constant for "f-``x" is now "vimage" rather than "op -``";
  6167 
  6168 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian
  6169 product is now "<*>" instead of "Times"; the lexicographic product is
  6170 now "<*lex*>" instead of "**";
  6171 
  6172 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part
  6173 of main HOL, but was unused); better use HOL's datatype package;
  6174 
  6175 * HOL: removed "symbols" syntax for constant "override" of theory Map;
  6176 the old syntax may be recovered as follows:
  6177 
  6178   syntax (symbols)
  6179     override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
  6180       (infixl "\\<oplus>" 100)
  6181 
  6182 * HOL/Real: "rabs" replaced by overloaded "abs" function;
  6183 
  6184 * HOL/ML: even fewer consts are declared as global (see theories Ord,
  6185 Lfp, Gfp, WF); this only affects ML packages that refer to const names
  6186 internally;
  6187 
  6188 * HOL and ZF: syntax for quotienting wrt an equivalence relation
  6189 changed from A/r to A//r;
  6190 
  6191 * ZF: new treatment of arithmetic (nat & int) may break some old
  6192 proofs;
  6193 
  6194 * Isar: renamed some attributes (RS -> THEN, simplify -> simplified,
  6195 rulify -> rule_format, elimify -> elim_format, ...);
  6196 
  6197 * Isar/Provers: intro/elim/dest attributes changed; renamed
  6198 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
  6199 should have to change intro!! to intro? only); replaced "delrule" by
  6200 "rule del";
  6201 
  6202 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
  6203 
  6204 * Provers: strengthened force_tac by using new first_best_tac;
  6205 
  6206 * LaTeX document preparation: several changes of isabelle.sty (see
  6207 lib/texinputs);
  6208 
  6209 
  6210 *** Document preparation ***
  6211 
  6212 * formal comments (text blocks etc.) in new-style theories may now
  6213 contain antiquotations of thm/prop/term/typ/text to be presented
  6214 according to latex print mode; concrete syntax is like this:
  6215 @{term[show_types] "f(x) = a + x"};
  6216 
  6217 * isatool mkdir provides easy setup of Isabelle session directories,
  6218 including proper document sources;
  6219 
  6220 * generated LaTeX sources are now deleted after successful run
  6221 (isatool document -c); may retain a copy somewhere else via -D option
  6222 of isatool usedir;
  6223 
  6224 * isatool usedir -D now lets isatool latex -o sty update the Isabelle
  6225 style files, achieving self-contained LaTeX sources and simplifying
  6226 LaTeX debugging;
  6227 
  6228 * old-style theories now produce (crude) LaTeX output as well;
  6229 
  6230 * browser info session directories are now self-contained (may be put
  6231 on WWW server seperately); improved graphs of nested sessions; removed
  6232 graph for 'all sessions';
  6233 
  6234 * several improvements in isabelle style files; \isabellestyle{it}
  6235 produces fake math mode output; \isamarkupheader is now \section by
  6236 default; see lib/texinputs/isabelle.sty etc.;
  6237