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