NEWS
author nipkow
Mon Apr 16 19:01:57 2012 +0200 (2012-04-16)
changeset 47495 573ca05db948
parent 47494 8c8f27864ed1
parent 47484 e94cc23d434a
child 47496 a43f207f216f
permissions -rw-r--r--
merged
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     3 
     4 New in Isabelle2012 (May 2012)
     5 ------------------------------
     6 
     7 *** General ***
     8 
     9 * Prover IDE (PIDE) improvements:
    10 
    11   - markup for bound variables
    12   - markup for types of term variables (e.g. displayed as tooltips)
    13   - support for user-defined Isar commands within the running session
    14   - improved support for Unicode outside original 16bit range
    15     e.g. glyph for \<A> (thanks to jEdit 4.5.1)
    16 
    17 * Updated and extended reference manuals ("isar-ref" and
    18 "implementation"); reduced remaining material in old "ref" manual.
    19 
    20 * Rule attributes in local theory declarations (e.g. locale or class)
    21 are now statically evaluated: the resulting theorem is stored instead
    22 of the original expression.  INCOMPATIBILITY in rare situations, where
    23 the historic accident of dynamic re-evaluation in interpretations
    24 etc. was exploited.
    25 
    26 * Commands 'lemmas' and 'theorems' allow local variables using 'for'
    27 declaration, and results are standardized before being stored.  Thus
    28 old-style "standard" after instantiation or composition of facts
    29 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    30 indices of schematic variables.
    31 
    32 * Renamed some inner syntax categories:
    33 
    34     num ~> num_token
    35     xnum ~> xnum_token
    36     xstr ~> str_token
    37 
    38 Minor INCOMPATIBILITY.  Note that in practice "num_const" or
    39 "num_position" etc. are mainly used instead (which also include
    40 position information via constraints).
    41 
    42 * Simplified configuration options for syntax ambiguity: see
    43 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    44 manual.  Minor INCOMPATIBILITY.
    45 
    46 * Forward declaration of outer syntax keywords within the theory
    47 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
    48 commands to be used in the same theory where defined.
    49 
    50 
    51 *** Pure ***
    52 
    53 * Auxiliary contexts indicate block structure for specifications with
    54 additional parameters and assumptions.  Such unnamed contexts may be
    55 nested within other targets, like 'theory', 'locale', 'class',
    56 'instantiation' etc.  Results from the local context are generalized
    57 accordingly and applied to the enclosing target context.  Example:
    58 
    59   context
    60     fixes x y z :: 'a
    61     assumes xy: "x = y" and yz: "y = z"
    62   begin
    63 
    64   lemma my_trans: "x = z" using xy yz by simp
    65 
    66   end
    67 
    68   thm my_trans
    69 
    70 The most basic application is to factor-out context elements of
    71 several fixes/assumes/shows theorem statements, e.g. see
    72 ~~/src/HOL/Isar_Examples/Group_Context.thy
    73 
    74 Any other local theory specification element works within the "context
    75 ... begin ... end" block as well.
    76 
    77 * Bundled declarations associate attributed fact expressions with a
    78 given name in the context.  These may be later included in other
    79 contexts.  This allows to manage context extensions casually, without
    80 the logical dependencies of locales and locale interpretation.
    81 
    82 See commands 'bundle', 'include', 'including' etc. in the isar-ref
    83 manual.
    84 
    85 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
    86 tolerant against multiple unifiers, as long as the final result is
    87 unique.  (As before, rules are composed in canonical right-to-left
    88 order to accommodate newly introduced premises.)
    89 
    90 * Command 'definition' no longer exports the foundational "raw_def"
    91 into the user context.  Minor INCOMPATIBILITY, may use the regular
    92 "def" result with attribute "abs_def" to imitate the old version.
    93 
    94 * Attribute "abs_def" turns an equation of the form "f x y == t" into
    95 "f == %x y. t", which ensures that "simp" or "unfold" steps always
    96 expand it.  This also works for object-logic equality.  (Formerly
    97 undocumented feature.)
    98 
    99 * Discontinued old "prems" fact, which used to refer to the accidental
   100 collection of foundational premises in the context (already marked as
   101 legacy since Isabelle2011).
   102 
   103 * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
   104 instead.  INCOMPATIBILITY.
   105 
   106 * Old code generator for SML and its commands 'code_module',
   107 'code_library', 'consts_code', 'types_code' have been discontinued.
   108 Use commands of the generic code generator instead.  INCOMPATIBILITY.
   109 
   110 * Redundant attribute "code_inline" has been discontinued. Use
   111 "code_unfold" instead.  INCOMPATIBILITY.
   112 
   113 * Dropped attribute "code_unfold_post" in favor of the its dual
   114 "code_abbrev", which yields a common pattern in definitions like
   115 
   116   definition [code_abbrev]: "f = t"
   117 
   118 INCOMPATIBILITY.
   119 
   120 * Sort constraints are now propagated in simultaneous statements, just
   121 like type constraints.  INCOMPATIBILITY in rare situations, where
   122 distinct sorts used to be assigned accidentally.  For example:
   123 
   124   lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"
   125 
   126   lemma "P (x::'a)" and "Q (y::'a::bar)"
   127     -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
   128 
   129 
   130 *** HOL ***
   131 
   132 
   133 * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").
   134 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
   135 which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
   136 for Higher-Order Logic" as the recommended beginners tutorial
   137 but does not cover all of the material of that old tutorial.
   138 
   139 * Discontinued old Tutorial on Isar ("isar-overview");
   140 
   141 * The representation of numerals has changed. We now have a datatype
   142 "num" representing strictly positive binary numerals, along with
   143 functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
   144 represent positive and negated numeric literals, respectively. (See
   145 definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories
   146 may require adaptations:
   147 
   148   - Theorems with number_ring or number_semiring constraints: These
   149     classes are gone; use comm_ring_1 or comm_semiring_1 instead.
   150 
   151   - Theories defining numeric types: Remove number, number_semiring,
   152     and number_ring instances. Defer all theorems about numerals until
   153     after classes one and semigroup_add have been instantiated.
   154 
   155   - Numeral-only simp rules: Replace each rule having a "number_of v"
   156     pattern with two copies, one for numeral and one for neg_numeral.
   157 
   158   - Theorems about subclasses of semiring_1 or ring_1: These classes
   159     automatically support numerals now, so more simp rules and
   160     simprocs may now apply within the proof.
   161 
   162   - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
   163     Redefine using other integer operations.
   164 
   165 * Type 'a set is now a proper type constructor (just as before
   166 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
   167 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
   168 sets separate, it is often sufficient to rephrase sets S accidentally
   169 used as predicates by "%x. x : S" and predicates P accidentally used
   170 as sets by "{x. P x}".  Corresponding proofs in a first step should be
   171 pruned from any tinkering with former theorems mem_def and Collect_def
   172 as far as possible.
   173 
   174 For developments which deliberately mixed predicates and sets, a
   175 planning step is necessary to determine what should become a predicate
   176 and what a set.  It can be helpful to carry out that step in
   177 Isabelle2011-1 before jumping right into the current release.
   178 
   179 * The representation of numerals has changed.  Datatype "num"
   180 represents strictly positive binary numerals, along with functions
   181 "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
   182 positive and negated numeric literals, respectively. (See definitions
   183 in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories
   184 may require adaptations as follows:
   185 
   186   - Theorems with number_ring or number_semiring constraints: These
   187     classes are gone; use comm_ring_1 or comm_semiring_1 instead.
   188 
   189   - Theories defining numeric types: Remove number, number_semiring,
   190     and number_ring instances. Defer all theorems about numerals until
   191     after classes one and semigroup_add have been instantiated.
   192 
   193   - Numeral-only simp rules: Replace each rule having a "number_of v"
   194     pattern with two copies, one for numeral and one for neg_numeral.
   195 
   196   - Theorems about subclasses of semiring_1 or ring_1: These classes
   197     automatically support numerals now, so more simp rules and
   198     simprocs may now apply within the proof.
   199 
   200   - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
   201     Redefine using other integer operations.
   202 
   203 * Code generation by default implements sets as container type rather
   204 than predicates.  INCOMPATIBILITY.
   205 
   206 * New proof import from HOL Light: Faster, simpler, and more scalable.
   207 Requires a proof bundle, which is available as an external component.
   208 Discontinued old (and mostly dead) Importer for HOL4 and HOL Light.
   209 INCOMPATIBILITY.
   210 
   211 * New type synonym 'a rel = ('a * 'a) set
   212 
   213 * Theory Divides: Discontinued redundant theorems about div and mod.
   214 INCOMPATIBILITY, use the corresponding generic theorems instead.
   215 
   216   DIVISION_BY_ZERO ~> div_by_0, mod_by_0
   217   zdiv_self ~> div_self
   218   zmod_self ~> mod_self
   219   zdiv_zero ~> div_0
   220   zmod_zero ~> mod_0
   221   zdiv_zmod_equality ~> div_mod_equality2
   222   zdiv_zmod_equality2 ~> div_mod_equality
   223   zmod_zdiv_trivial ~> mod_div_trivial
   224   zdiv_zminus_zminus ~> div_minus_minus
   225   zmod_zminus_zminus ~> mod_minus_minus
   226   zdiv_zminus2 ~> div_minus_right
   227   zmod_zminus2 ~> mod_minus_right
   228   zdiv_minus1_right ~> div_minus1_right
   229   zmod_minus1_right ~> mod_minus1_right
   230   zdvd_mult_div_cancel ~> dvd_mult_div_cancel
   231   zmod_zmult1_eq ~> mod_mult_right_eq
   232   zpower_zmod ~> power_mod
   233   zdvd_zmod ~> dvd_mod
   234   zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
   235   mod_mult_distrib ~> mult_mod_left
   236   mod_mult_distrib2 ~> mult_mod_right
   237 
   238 * Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
   239 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
   240 
   241 * More default pred/set conversions on a couple of relation operations
   242 and predicates.  Added powers of predicate relations.  Consolidation
   243 of some relation theorems:
   244 
   245   converse_def ~> converse_unfold
   246   rel_comp_def ~> rel_comp_unfold
   247   symp_def ~> (dropped, use symp_def and sym_def instead)
   248   transp_def ~> transp_trans
   249   Domain_def ~> Domain_unfold
   250   Range_def ~> Domain_converse [symmetric]
   251 
   252 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
   253 
   254 See theory "Relation" for examples for making use of pred/set
   255 conversions by means of attributes "to_set" and "to_pred".
   256 
   257 INCOMPATIBILITY.
   258 
   259 * Consolidated various theorem names relating to Finite_Set.fold
   260 combinator:
   261 
   262   inf_INFI_fold_inf ~> inf_INF_fold_inf
   263   sup_SUPR_fold_sup ~> sup_SUP_fold_sup
   264   INFI_fold_inf ~> INF_fold_inf
   265   SUPR_fold_sup ~> SUP_fold_sup
   266   union_set ~> union_set_fold
   267   minus_set ~> minus_set_fold
   268 
   269 INCOMPATIBILITY.
   270 
   271 * Consolidated theorem names concerning fold combinators:
   272 
   273   INFI_set_fold ~> INF_set_fold
   274   SUPR_set_fold ~> SUP_set_fold
   275   INF_code ~> INF_set_foldr
   276   SUP_code ~> SUP_set_foldr
   277   foldr.simps ~> foldr.simps (in point-free formulation)
   278   foldr_fold_rev ~> foldr_conv_fold
   279   foldl_fold ~> foldl_conv_fold
   280   foldr_foldr ~> foldr_conv_foldl
   281   foldl_foldr ~> foldl_conv_foldr
   282 
   283 INCOMPATIBILITY.
   284 
   285 * Dropped rarely useful theorems concerning fold combinators:
   286 foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
   287 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
   288 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
   289 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
   290 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
   291 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
   292 INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
   293 and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can be
   294 useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
   295 unfolding "foldr_conv_fold" and "foldl_conv_fold".
   296 
   297 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
   298 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
   299 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
   300 INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding
   301 lemmas over fold rather than foldr, or make use of lemmas
   302 fold_conv_foldr and fold_rev.
   303 
   304 * Congruence rules Option.map_cong and Option.bind_cong for recursion
   305 through option types.
   306 
   307 * Concrete syntax for case expressions includes constraints for source
   308 positions, and thus produces Prover IDE markup for its bindings.
   309 INCOMPATIBILITY for old-style syntax translations that augment the
   310 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
   311 one_case.
   312 
   313 * Discontinued configuration option "syntax_positions": atomic terms
   314 in parse trees are always annotated by position constraints.
   315 
   316 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
   317 
   318 * Renamed some facts on canonical fold on lists, in order to avoid
   319 problems with interpretation involving corresponding facts on foldl
   320 with the same base names:
   321 
   322   fold_set_remdups ~> fold_set_fold_remdups
   323   fold_set ~> fold_set_fold
   324   fold1_set ~> fold1_set_fold
   325 
   326 INCOMPATIBILITY.
   327 
   328 * Renamed facts about the power operation on relations, i.e., relpow
   329 to match the constant's name:
   330 
   331   rel_pow_1 ~> relpow_1
   332   rel_pow_0_I ~> relpow_0_I
   333   rel_pow_Suc_I ~> relpow_Suc_I
   334   rel_pow_Suc_I2 ~> relpow_Suc_I2
   335   rel_pow_0_E ~> relpow_0_E
   336   rel_pow_Suc_E ~> relpow_Suc_E
   337   rel_pow_E ~> relpow_E
   338   rel_pow_Suc_D2 ~> relpow_Suc_D2
   339   rel_pow_Suc_E2 ~> relpow_Suc_E2
   340   rel_pow_Suc_D2' ~> relpow_Suc_D2'
   341   rel_pow_E2 ~> relpow_E2
   342   rel_pow_add ~> relpow_add
   343   rel_pow_commute ~> relpow
   344   rel_pow_empty ~> relpow_empty:
   345   rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow
   346   rel_pow_imp_rtrancl ~> relpow_imp_rtrancl
   347   rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow
   348   rtrancl_imp_rel_pow ~> rtrancl_imp_relpow
   349   rel_pow_fun_conv ~> relpow_fun_conv
   350   rel_pow_finite_bounded1 ~> relpow_finite_bounded1
   351   rel_pow_finite_bounded ~> relpow_finite_bounded
   352   rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow
   353   trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow
   354   single_valued_rel_pow ~> single_valued_relpow
   355 
   356 INCOMPATIBILITY.
   357 
   358 * Theory Relation: Consolidated constant name for relation composition
   359 and corresponding theorem names:
   360 
   361   - Renamed constant rel_comp to relcomp
   362 
   363   - Dropped abbreviation pred_comp. Use relcompp instead.
   364 
   365   - Renamed theorems:
   366 
   367     rel_compI ~> relcompI
   368     rel_compEpair ~> relcompEpair
   369     rel_compE ~> relcompE
   370     pred_comp_rel_comp_eq ~> relcompp_relcomp_eq
   371     rel_comp_empty1 ~> relcomp_empty1
   372     rel_comp_mono ~> relcomp_mono
   373     rel_comp_subset_Sigma ~> relcomp_subset_Sigma
   374     rel_comp_distrib ~> relcomp_distrib
   375     rel_comp_distrib2 ~> relcomp_distrib2
   376     rel_comp_UNION_distrib ~> relcomp_UNION_distrib
   377     rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
   378     single_valued_rel_comp ~> single_valued_relcomp
   379     rel_comp_unfold ~> relcomp_unfold
   380     converse_rel_comp ~> converse_relcomp
   381     pred_compI ~> relcomppI
   382     pred_compE ~> relcomppE
   383     pred_comp_bot1 ~> relcompp_bot1
   384     pred_comp_bot2 ~> relcompp_bot2
   385     transp_pred_comp_less_eq ~> transp_relcompp_less_eq
   386     pred_comp_mono ~> relcompp_mono
   387     pred_comp_distrib ~> relcompp_distrib
   388     pred_comp_distrib2 ~> relcompp_distrib2
   389     converse_pred_comp ~> converse_relcompp
   390 
   391     finite_rel_comp ~> finite_relcomp
   392 
   393     set_rel_comp ~> set_relcomp
   394 
   395 INCOMPATIBILITY.
   396 
   397 * New theory HOL/Library/DAList provides an abstract type for
   398 association lists with distinct keys.
   399 
   400 * 'datatype' specifications allow explicit sort constraints.
   401 
   402 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
   403 use theory HOL/Library/Nat_Bijection instead.
   404 
   405 * Theory HOL/Library/RBT_Impl: Backing implementation of red-black
   406 trees is now inside a type class context.  Names of affected
   407 operations and lemmas have been prefixed by rbt_.  INCOMPATIBILITY for
   408 theories working directly with raw red-black trees, adapt the names as
   409 follows:
   410 
   411   Operations:
   412   bulkload -> rbt_bulkload
   413   del_from_left -> rbt_del_from_left
   414   del_from_right -> rbt_del_from_right
   415   del -> rbt_del
   416   delete -> rbt_delete
   417   ins -> rbt_ins
   418   insert -> rbt_insert
   419   insertw -> rbt_insert_with
   420   insert_with_key -> rbt_insert_with_key
   421   map_entry -> rbt_map_entry
   422   lookup -> rbt_lookup
   423   sorted -> rbt_sorted
   424   tree_greater -> rbt_greater
   425   tree_less -> rbt_less
   426   tree_less_symbol -> rbt_less_symbol
   427   union -> rbt_union
   428   union_with -> rbt_union_with
   429   union_with_key -> rbt_union_with_key
   430 
   431   Lemmas:
   432   balance_left_sorted -> balance_left_rbt_sorted
   433   balance_left_tree_greater -> balance_left_rbt_greater
   434   balance_left_tree_less -> balance_left_rbt_less
   435   balance_right_sorted -> balance_right_rbt_sorted
   436   balance_right_tree_greater -> balance_right_rbt_greater
   437   balance_right_tree_less -> balance_right_rbt_less
   438   balance_sorted -> balance_rbt_sorted
   439   balance_tree_greater -> balance_rbt_greater
   440   balance_tree_less -> balance_rbt_less
   441   bulkload_is_rbt -> rbt_bulkload_is_rbt
   442   combine_sorted -> combine_rbt_sorted
   443   combine_tree_greater -> combine_rbt_greater
   444   combine_tree_less -> combine_rbt_less
   445   delete_in_tree -> rbt_delete_in_tree
   446   delete_is_rbt -> rbt_delete_is_rbt
   447   del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
   448   del_from_left_tree_less -> rbt_del_from_left_rbt_less
   449   del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
   450   del_from_right_tree_less -> rbt_del_from_right_rbt_less
   451   del_in_tree -> rbt_del_in_tree
   452   del_inv1_inv2 -> rbt_del_inv1_inv2
   453   del_sorted -> rbt_del_rbt_sorted
   454   del_tree_greater -> rbt_del_rbt_greater
   455   del_tree_less -> rbt_del_rbt_less
   456   dom_lookup_Branch -> dom_rbt_lookup_Branch
   457   entries_lookup -> entries_rbt_lookup
   458   finite_dom_lookup -> finite_dom_rbt_lookup
   459   insert_sorted -> rbt_insert_rbt_sorted
   460   insertw_is_rbt -> rbt_insertw_is_rbt
   461   insertwk_is_rbt -> rbt_insertwk_is_rbt
   462   insertwk_sorted -> rbt_insertwk_rbt_sorted
   463   insertw_sorted -> rbt_insertw_rbt_sorted
   464   ins_sorted -> ins_rbt_sorted
   465   ins_tree_greater -> ins_rbt_greater
   466   ins_tree_less -> ins_rbt_less
   467   is_rbt_sorted -> is_rbt_rbt_sorted
   468   lookup_balance -> rbt_lookup_balance
   469   lookup_bulkload -> rbt_lookup_rbt_bulkload
   470   lookup_delete -> rbt_lookup_rbt_delete
   471   lookup_Empty -> rbt_lookup_Empty
   472   lookup_from_in_tree -> rbt_lookup_from_in_tree
   473   lookup_in_tree -> rbt_lookup_in_tree
   474   lookup_ins -> rbt_lookup_ins
   475   lookup_insert -> rbt_lookup_rbt_insert
   476   lookup_insertw -> rbt_lookup_rbt_insertw
   477   lookup_insertwk -> rbt_lookup_rbt_insertwk
   478   lookup_keys -> rbt_lookup_keys
   479   lookup_map -> rbt_lookup_map
   480   lookup_map_entry -> rbt_lookup_rbt_map_entry
   481   lookup_tree_greater -> rbt_lookup_rbt_greater
   482   lookup_tree_less -> rbt_lookup_rbt_less
   483   lookup_union -> rbt_lookup_rbt_union
   484   map_entry_color_of -> rbt_map_entry_color_of
   485   map_entry_inv1 -> rbt_map_entry_inv1
   486   map_entry_inv2 -> rbt_map_entry_inv2
   487   map_entry_is_rbt -> rbt_map_entry_is_rbt
   488   map_entry_sorted -> rbt_map_entry_rbt_sorted
   489   map_entry_tree_greater -> rbt_map_entry_rbt_greater
   490   map_entry_tree_less -> rbt_map_entry_rbt_less
   491   map_tree_greater -> map_rbt_greater
   492   map_tree_less -> map_rbt_less
   493   map_sorted -> map_rbt_sorted
   494   paint_sorted -> paint_rbt_sorted
   495   paint_lookup -> paint_rbt_lookup
   496   paint_tree_greater -> paint_rbt_greater
   497   paint_tree_less -> paint_rbt_less
   498   sorted_entries -> rbt_sorted_entries
   499   tree_greater_eq_trans -> rbt_greater_eq_trans
   500   tree_greater_nit -> rbt_greater_nit
   501   tree_greater_prop -> rbt_greater_prop
   502   tree_greater_simps -> rbt_greater_simps
   503   tree_greater_trans -> rbt_greater_trans
   504   tree_less_eq_trans -> rbt_less_eq_trans
   505   tree_less_nit -> rbt_less_nit
   506   tree_less_prop -> rbt_less_prop
   507   tree_less_simps -> rbt_less_simps
   508   tree_less_trans -> rbt_less_trans
   509   tree_ord_props -> rbt_ord_props
   510   union_Branch -> rbt_union_Branch
   511   union_is_rbt -> rbt_union_is_rbt
   512   unionw_is_rbt -> rbt_unionw_is_rbt
   513   unionwk_is_rbt -> rbt_unionwk_is_rbt
   514   unionwk_sorted -> rbt_unionwk_rbt_sorted
   515 
   516 * Session HOL-Word: Discontinued many redundant theorems specific to
   517 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
   518 instead.
   519 
   520   word_sub_alt ~> word_sub_wi
   521   word_add_alt ~> word_add_def
   522   word_mult_alt ~> word_mult_def
   523   word_minus_alt ~> word_minus_def
   524   word_0_alt ~> word_0_wi
   525   word_1_alt ~> word_1_wi
   526   word_add_0 ~> add_0_left
   527   word_add_0_right ~> add_0_right
   528   word_mult_1 ~> mult_1_left
   529   word_mult_1_right ~> mult_1_right
   530   word_add_commute ~> add_commute
   531   word_add_assoc ~> add_assoc
   532   word_add_left_commute ~> add_left_commute
   533   word_mult_commute ~> mult_commute
   534   word_mult_assoc ~> mult_assoc
   535   word_mult_left_commute ~> mult_left_commute
   536   word_left_distrib ~> left_distrib
   537   word_right_distrib ~> right_distrib
   538   word_left_minus ~> left_minus
   539   word_diff_0_right ~> diff_0_right
   540   word_diff_self ~> diff_self
   541   word_sub_def ~> diff_minus
   542   word_diff_minus ~> diff_minus
   543   word_add_ac ~> add_ac
   544   word_mult_ac ~> mult_ac
   545   word_plus_ac0 ~> add_0_left add_0_right add_ac
   546   word_times_ac1 ~> mult_1_left mult_1_right mult_ac
   547   word_order_trans ~> order_trans
   548   word_order_refl ~> order_refl
   549   word_order_antisym ~> order_antisym
   550   word_order_linear ~> linorder_linear
   551   lenw1_zero_neq_one ~> zero_neq_one
   552   word_number_of_eq ~> number_of_eq
   553   word_of_int_add_hom ~> wi_hom_add
   554   word_of_int_sub_hom ~> wi_hom_sub
   555   word_of_int_mult_hom ~> wi_hom_mult
   556   word_of_int_minus_hom ~> wi_hom_neg
   557   word_of_int_succ_hom ~> wi_hom_succ
   558   word_of_int_pred_hom ~> wi_hom_pred
   559   word_of_int_0_hom ~> word_0_wi
   560   word_of_int_1_hom ~> word_1_wi
   561 
   562 * Clarified attribute "mono_set": pure declaration without modifying
   563 the result of the fact expression.
   564 
   565 * "Transitive_Closure.ntrancl": bounded transitive closure on
   566 relations.
   567 
   568 * Constant "Set.not_member" now qualified.  INCOMPATIBILITY.
   569 
   570 * "sublists" moved to theory More_List.  INCOMPATIBILITY.
   571 
   572 * Theory Int: Discontinued many legacy theorems specific to type int.
   573 INCOMPATIBILITY, use the corresponding generic theorems instead.
   574 
   575   zminus_zminus ~> minus_minus
   576   zminus_0 ~> minus_zero
   577   zminus_zadd_distrib ~> minus_add_distrib
   578   zadd_commute ~> add_commute
   579   zadd_assoc ~> add_assoc
   580   zadd_left_commute ~> add_left_commute
   581   zadd_ac ~> add_ac
   582   zmult_ac ~> mult_ac
   583   zadd_0 ~> add_0_left
   584   zadd_0_right ~> add_0_right
   585   zadd_zminus_inverse2 ~> left_minus
   586   zmult_zminus ~> mult_minus_left
   587   zmult_commute ~> mult_commute
   588   zmult_assoc ~> mult_assoc
   589   zadd_zmult_distrib ~> left_distrib
   590   zadd_zmult_distrib2 ~> right_distrib
   591   zdiff_zmult_distrib ~> left_diff_distrib
   592   zdiff_zmult_distrib2 ~> right_diff_distrib
   593   zmult_1 ~> mult_1_left
   594   zmult_1_right ~> mult_1_right
   595   zle_refl ~> order_refl
   596   zle_trans ~> order_trans
   597   zle_antisym ~> order_antisym
   598   zle_linear ~> linorder_linear
   599   zless_linear ~> linorder_less_linear
   600   zadd_left_mono ~> add_left_mono
   601   zadd_strict_right_mono ~> add_strict_right_mono
   602   zadd_zless_mono ~> add_less_le_mono
   603   int_0_less_1 ~> zero_less_one
   604   int_0_neq_1 ~> zero_neq_one
   605   zless_le ~> less_le
   606   zpower_zadd_distrib ~> power_add
   607   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
   608   zero_le_zpower_abs ~> zero_le_power_abs
   609 
   610 * Theory Deriv: Renamed
   611 
   612   DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
   613 
   614 * New "case_product" attribute to generate a case rule doing multiple
   615 case distinctions at the same time.  E.g.
   616 
   617   list.exhaust [case_product nat.exhaust]
   618 
   619 produces a rule which can be used to perform case distinction on both
   620 a list and a nat.
   621 
   622 * Theory Library/Multiset: Improved code generation of multisets.
   623 
   624 * New diagnostic command 'find_unused_assms' to find potentially
   625 superfluous assumptions in theorems using Quickcheck.
   626 
   627 * Quickcheck:
   628 
   629   - Quickcheck returns variable assignments as counterexamples, which
   630     allows to reveal the underspecification of functions under test.
   631     For example, refuting "hd xs = x", it presents the variable
   632     assignment xs = [] and x = a1 as a counterexample, assuming that
   633     any property is false whenever "hd []" occurs in it.
   634 
   635     These counterexample are marked as potentially spurious, as
   636     Quickcheck also returns "xs = []" as a counterexample to the
   637     obvious theorem "hd xs = hd xs".
   638 
   639     After finding a potentially spurious counterexample, Quickcheck
   640     continues searching for genuine ones.
   641 
   642     By default, Quickcheck shows potentially spurious and genuine
   643     counterexamples. The option "genuine_only" sets quickcheck to only
   644     show genuine counterexamples.
   645 
   646   - The command 'quickcheck_generator' creates random and exhaustive
   647     value generators for a given type and operations.
   648 
   649     It generates values by using the operations as if they were
   650     constructors of that type.
   651 
   652   - Support for multisets.
   653 
   654   - Added "use_subtype" options.
   655 
   656   - Added "quickcheck_locale" configuration to specify how to process
   657     conjectures in a locale context.
   658 
   659 * Nitpick:
   660 
   661   - Fixed infinite loop caused by the 'peephole_optim' option and
   662     affecting 'rat' and 'real'.
   663 
   664 * Sledgehammer:
   665   - Added "lam_trans", "uncurry_aliases", and "minimize" options.
   666   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
   667   - Renamed "sound" option to "strict".
   668 
   669 * Metis:
   670   - Added possibility to specify lambda translations scheme as a
   671     parenthesized argument (e.g., "by (metis (lifting) ...)").
   672 
   673 * SMT:
   674   - renamed "smt_fixed" option to "smt_read_only_certificates".
   675 
   676 * Command 'try0':
   677   - Renamed from 'try_methods'. INCOMPATIBILITY.
   678 
   679 * New "eventually_elim" method as a generalized variant of the
   680 eventually_elim* rules. Supports structured proofs.
   681 
   682 * HOL/TPTP: support to parse and import TPTP problems (all languages)
   683 into Isabelle/HOL.
   684 
   685 
   686 *** FOL ***
   687 
   688 * New "case_product" attribute (see HOL).
   689 
   690 
   691 *** ZF ***
   692 
   693 * Greater support for structured proofs involving induction or case
   694 analysis.
   695 
   696 * Much greater use of mathematical symbols.
   697 
   698 * Removal of many ML theorem bindings.  INCOMPATIBILITY.
   699 
   700 
   701 *** ML ***
   702 
   703 * Antiquotation @{keyword "name"} produces a parser for outer syntax
   704 from a minor keyword introduced via theory header declaration.
   705 
   706 * Antiquotation @{command_spec "name"} produces the
   707 Outer_Syntax.command_spec from a major keyword introduced via theory
   708 header declaration; it can be passed to Outer_Syntax.command etc.
   709 
   710 * Local_Theory.define no longer hard-wires default theorem name
   711 "foo_def", but retains the binding as given.  If that is Binding.empty
   712 / Attrib.empty_binding, the result is not registered as user-level
   713 fact.  The Local_Theory.define_internal variant allows to specify a
   714 non-empty name (used for the foundation in the background theory),
   715 while omitting the fact binding in the user-context.  Potential
   716 INCOMPATIBILITY for derived definitional packages: need to specify
   717 naming policy for primitive definitions more explicitly.
   718 
   719 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
   720 conformance with similar operations in structure Term and Logic.
   721 
   722 * Antiquotation @{attributes [...]} embeds attribute source
   723 representation into the ML text, which is particularly useful with
   724 declarations like Local_Theory.note.
   725 
   726 * Structure Proof_Context follows standard naming scheme.  Old
   727 ProofContext has been discontinued.  INCOMPATIBILITY.
   728 
   729 * Refined Local_Theory.declaration {syntax, pervasive}, with subtle
   730 change of semantics: update is applied to auxiliary local theory
   731 context as well.
   732 
   733 * Modernized some old-style infix operations:
   734 
   735   addeqcongs    ~> Simplifier.add_eqcong
   736   deleqcongs    ~> Simplifier.del_eqcong
   737   addcongs      ~> Simplifier.add_cong
   738   delcongs      ~> Simplifier.del_cong
   739   setmksimps    ~> Simplifier.set_mksimps
   740   setmkcong     ~> Simplifier.set_mkcong
   741   setmksym      ~> Simplifier.set_mksym
   742   setmkeqTrue   ~> Simplifier.set_mkeqTrue
   743   settermless   ~> Simplifier.set_termless
   744   setsubgoaler  ~> Simplifier.set_subgoaler
   745   addsplits     ~> Splitter.add_split
   746   delsplits     ~> Splitter.del_split
   747 
   748 
   749 *** System ***
   750 
   751 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
   752 (not just JRE).
   753 
   754 * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
   755 notation, which is useful for the jEdit file browser, for example.
   756 
   757 
   758 
   759 New in Isabelle2011-1 (October 2011)
   760 ------------------------------------
   761 
   762 *** General ***
   763 
   764 * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
   765 "isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.
   766 
   767   - Management of multiple theory files directly from the editor
   768     buffer store -- bypassing the file-system (no requirement to save
   769     files for checking).
   770 
   771   - Markup of formal entities within the text buffer, with semantic
   772     highlighting, tooltips and hyperlinks to jump to defining source
   773     positions.
   774 
   775   - Improved text rendering, with sub/superscripts in the source
   776     buffer (including support for copy/paste wrt. output panel, HTML
   777     theory output and other non-Isabelle text boxes).
   778 
   779   - Refined scheduling of proof checking and printing of results,
   780     based on interactive editor view.  (Note: jEdit folding and
   781     narrowing allows to restrict buffer perspectives explicitly.)
   782 
   783   - Reduced CPU performance requirements, usable on machines with few
   784     cores.
   785 
   786   - Reduced memory requirements due to pruning of unused document
   787     versions (garbage collection).
   788 
   789 See also ~~/src/Tools/jEdit/README.html for further information,
   790 including some remaining limitations.
   791 
   792 * Theory loader: source files are exclusively located via the master
   793 directory of each theory node (where the .thy file itself resides).
   794 The global load path (such as src/HOL/Library) has been discontinued.
   795 Note that the path element ~~ may be used to reference theories in the
   796 Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
   797 INCOMPATIBILITY.
   798 
   799 * Theory loader: source files are identified by content via SHA1
   800 digests.  Discontinued former path/modtime identification and optional
   801 ISABELLE_FILE_IDENT plugin scripts.
   802 
   803 * Parallelization of nested Isar proofs is subject to
   804 Goal.parallel_proofs_threshold (default 100).  See also isabelle
   805 usedir option -Q.
   806 
   807 * Name space: former unsynchronized references are now proper
   808 configuration options, with more conventional names:
   809 
   810   long_names   ~> names_long
   811   short_names  ~> names_short
   812   unique_names ~> names_unique
   813 
   814 Minor INCOMPATIBILITY, need to declare options in context like this:
   815 
   816   declare [[names_unique = false]]
   817 
   818 * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
   819 that the result needs to be unique, which means fact specifications
   820 may have to be refined after enriching a proof context.
   821 
   822 * Attribute "case_names" has been refined: the assumptions in each case
   823 can be named now by following the case name with [name1 name2 ...].
   824 
   825 * Isabelle/Isar reference manual has been updated and extended:
   826   - "Synopsis" provides a catalog of main Isar language concepts.
   827   - Formal references in syntax diagrams, via @{rail} antiquotation.
   828   - Updated material from classic "ref" manual, notably about
   829     "Classical Reasoner".
   830 
   831 
   832 *** HOL ***
   833 
   834 * Class bot and top require underlying partial order rather than
   835 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
   836 
   837 * Class complete_lattice: generalized a couple of lemmas from sets;
   838 generalized theorems INF_cong and SUP_cong.  New type classes for
   839 complete boolean algebras and complete linear orders.  Lemmas
   840 Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in
   841 class complete_linorder.
   842 
   843 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,
   844 Sup_fun_def, Inf_apply, Sup_apply.
   845 
   846 Removed redundant lemmas (the right hand side gives hints how to
   847 replace them for (metis ...), or (simp only: ...) proofs):
   848 
   849   Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
   850   Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
   851   Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right
   852   Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right
   853   Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right
   854   Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right
   855   Inter_def ~> INF_def, image_def
   856   Union_def ~> SUP_def, image_def
   857   INT_eq ~> INF_def, and image_def
   858   UN_eq ~> SUP_def, and image_def
   859   INF_subset ~> INF_superset_mono [OF _ order_refl]
   860 
   861 More consistent and comprehensive names:
   862 
   863   INTER_eq_Inter_image ~> INF_def
   864   UNION_eq_Union_image ~> SUP_def
   865   INFI_def ~> INF_def
   866   SUPR_def ~> SUP_def
   867   INF_leI ~> INF_lower
   868   INF_leI2 ~> INF_lower2
   869   le_INFI ~> INF_greatest
   870   le_SUPI ~> SUP_upper
   871   le_SUPI2 ~> SUP_upper2
   872   SUP_leI ~> SUP_least
   873   INFI_bool_eq ~> INF_bool_eq
   874   SUPR_bool_eq ~> SUP_bool_eq
   875   INFI_apply ~> INF_apply
   876   SUPR_apply ~> SUP_apply
   877   INTER_def ~> INTER_eq
   878   UNION_def ~> UNION_eq
   879 
   880 INCOMPATIBILITY.
   881 
   882 * Renamed theory Complete_Lattice to Complete_Lattices.
   883 INCOMPATIBILITY.
   884 
   885 * Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,
   886 INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,
   887 Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,
   888 Sup_insert are now declared as [simp].  INCOMPATIBILITY.
   889 
   890 * Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,
   891 compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,
   892 sup_inf_absob, sup_left_idem are now declared as [simp].  Minor
   893 INCOMPATIBILITY.
   894 
   895 * Added syntactic classes "inf" and "sup" for the respective
   896 constants.  INCOMPATIBILITY: Changes in the argument order of the
   897 (mostly internal) locale predicates for some derived classes.
   898 
   899 * Theorem collections ball_simps and bex_simps do not contain theorems
   900 referring to UNION any longer; these have been moved to collection
   901 UN_ball_bex_simps.  INCOMPATIBILITY.
   902 
   903 * Theory Archimedean_Field: floor now is defined as parameter of a
   904 separate type class floor_ceiling.
   905 
   906 * Theory Finite_Set: more coherent development of fold_set locales:
   907 
   908     locale fun_left_comm ~> locale comp_fun_commute
   909     locale fun_left_comm_idem ~> locale comp_fun_idem
   910 
   911 Both use point-free characterization; interpretation proofs may need
   912 adjustment.  INCOMPATIBILITY.
   913 
   914 * Theory Limits: Type "'a net" has been renamed to "'a filter", in
   915 accordance with standard mathematical terminology. INCOMPATIBILITY.
   916 
   917 * Theory Complex_Main: The locale interpretations for the
   918 bounded_linear and bounded_bilinear locales have been removed, in
   919 order to reduce the number of duplicate lemmas. Users must use the
   920 original names for distributivity theorems, potential INCOMPATIBILITY.
   921 
   922   divide.add ~> add_divide_distrib
   923   divide.diff ~> diff_divide_distrib
   924   divide.setsum ~> setsum_divide_distrib
   925   mult.add_right ~> right_distrib
   926   mult.diff_right ~> right_diff_distrib
   927   mult_right.setsum ~> setsum_right_distrib
   928   mult_left.diff ~> left_diff_distrib
   929 
   930 * Theory Complex_Main: Several redundant theorems have been removed or
   931 replaced by more general versions. INCOMPATIBILITY.
   932 
   933   real_diff_def ~> minus_real_def
   934   real_divide_def ~> divide_real_def
   935   real_less_def ~> less_le
   936   real_abs_def ~> abs_real_def
   937   real_sgn_def ~> sgn_real_def
   938   real_mult_commute ~> mult_commute
   939   real_mult_assoc ~> mult_assoc
   940   real_mult_1 ~> mult_1_left
   941   real_add_mult_distrib ~> left_distrib
   942   real_zero_not_eq_one ~> zero_neq_one
   943   real_mult_inverse_left ~> left_inverse
   944   INVERSE_ZERO ~> inverse_zero
   945   real_le_refl ~> order_refl
   946   real_le_antisym ~> order_antisym
   947   real_le_trans ~> order_trans
   948   real_le_linear ~> linear
   949   real_le_eq_diff ~> le_iff_diff_le_0
   950   real_add_left_mono ~> add_left_mono
   951   real_mult_order ~> mult_pos_pos
   952   real_mult_less_mono2 ~> mult_strict_left_mono
   953   real_of_int_real_of_nat ~> real_of_int_of_nat_eq
   954   real_0_le_divide_iff ~> zero_le_divide_iff
   955   realpow_two_disj ~> power2_eq_iff
   956   real_squared_diff_one_factored ~> square_diff_one_factored
   957   realpow_two_diff ~> square_diff_square_factored
   958   reals_complete2 ~> complete_real
   959   real_sum_squared_expand ~> power2_sum
   960   exp_ln_eq ~> ln_unique
   961   expi_add ~> exp_add
   962   expi_zero ~> exp_zero
   963   lemma_DERIV_subst ~> DERIV_cong
   964   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
   965   LIMSEQ_const ~> tendsto_const
   966   LIMSEQ_norm ~> tendsto_norm
   967   LIMSEQ_add ~> tendsto_add
   968   LIMSEQ_minus ~> tendsto_minus
   969   LIMSEQ_minus_cancel ~> tendsto_minus_cancel
   970   LIMSEQ_diff ~> tendsto_diff
   971   bounded_linear.LIMSEQ ~> bounded_linear.tendsto
   972   bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto
   973   LIMSEQ_mult ~> tendsto_mult
   974   LIMSEQ_inverse ~> tendsto_inverse
   975   LIMSEQ_divide ~> tendsto_divide
   976   LIMSEQ_pow ~> tendsto_power
   977   LIMSEQ_setsum ~> tendsto_setsum
   978   LIMSEQ_setprod ~> tendsto_setprod
   979   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
   980   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
   981   LIMSEQ_imp_rabs ~> tendsto_rabs
   982   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
   983   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
   984   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
   985   LIMSEQ_Complex ~> tendsto_Complex
   986   LIM_ident ~> tendsto_ident_at
   987   LIM_const ~> tendsto_const
   988   LIM_add ~> tendsto_add
   989   LIM_add_zero ~> tendsto_add_zero
   990   LIM_minus ~> tendsto_minus
   991   LIM_diff ~> tendsto_diff
   992   LIM_norm ~> tendsto_norm
   993   LIM_norm_zero ~> tendsto_norm_zero
   994   LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel
   995   LIM_norm_zero_iff ~> tendsto_norm_zero_iff
   996   LIM_rabs ~> tendsto_rabs
   997   LIM_rabs_zero ~> tendsto_rabs_zero
   998   LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel
   999   LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff
  1000   LIM_compose ~> tendsto_compose
  1001   LIM_mult ~> tendsto_mult
  1002   LIM_scaleR ~> tendsto_scaleR
  1003   LIM_of_real ~> tendsto_of_real
  1004   LIM_power ~> tendsto_power
  1005   LIM_inverse ~> tendsto_inverse
  1006   LIM_sgn ~> tendsto_sgn
  1007   isCont_LIM_compose ~> isCont_tendsto_compose
  1008   bounded_linear.LIM ~> bounded_linear.tendsto
  1009   bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero
  1010   bounded_bilinear.LIM ~> bounded_bilinear.tendsto
  1011   bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero
  1012   bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero
  1013   bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
  1014   LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
  1015 
  1016 * Theory Complex_Main: The definition of infinite series was
  1017 generalized.  Now it is defined on the type class {topological_space,
  1018 comm_monoid_add}.  Hence it is useable also for extended real numbers.
  1019 
  1020 * Theory Complex_Main: The complex exponential function "expi" is now
  1021 a type-constrained abbreviation for "exp :: complex => complex"; thus
  1022 several polymorphic lemmas about "exp" are now applicable to "expi".
  1023 
  1024 * Code generation:
  1025 
  1026   - Theory Library/Code_Char_ord provides native ordering of
  1027     characters in the target language.
  1028 
  1029   - Commands code_module and code_library are legacy, use export_code
  1030     instead.
  1031 
  1032   - Method "evaluation" is legacy, use method "eval" instead.
  1033 
  1034   - Legacy evaluator "SML" is deactivated by default.  May be
  1035     reactivated by the following theory command:
  1036 
  1037       setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}
  1038 
  1039 * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
  1040 
  1041 * New proof method "induction" that gives induction hypotheses the
  1042 name "IH", thus distinguishing them from further hypotheses that come
  1043 from rule induction.  The latter are still called "hyps".  Method
  1044 "induction" is a thin wrapper around "induct" and follows the same
  1045 syntax.
  1046 
  1047 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
  1048 still available as a legacy feature for some time.
  1049 
  1050 * Nitpick:
  1051   - Added "need" and "total_consts" options.
  1052   - Reintroduced "show_skolems" option by popular demand.
  1053   - Renamed attribute: nitpick_def ~> nitpick_unfold.
  1054     INCOMPATIBILITY.
  1055 
  1056 * Sledgehammer:
  1057   - Use quasi-sound (and efficient) translations by default.
  1058   - Added support for the following provers: E-ToFoF, LEO-II,
  1059     Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.
  1060   - Automatically preplay and minimize proofs before showing them if
  1061     this can be done within reasonable time.
  1062   - sledgehammer available_provers ~> sledgehammer supported_provers.
  1063     INCOMPATIBILITY.
  1064   - Added "preplay_timeout", "slicing", "type_enc", "sound",
  1065     "max_mono_iters", and "max_new_mono_instances" options.
  1066   - Removed "explicit_apply" and "full_types" options as well as "Full
  1067     Types" Proof General menu item. INCOMPATIBILITY.
  1068 
  1069 * Metis:
  1070   - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
  1071   - Obsoleted "metisFT" -- use "metis (full_types)" instead.
  1072     INCOMPATIBILITY.
  1073 
  1074 * Command 'try':
  1075   - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
  1076     "elim:" options. INCOMPATIBILITY.
  1077   - Introduced 'try' that not only runs 'try_methods' but also
  1078     'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
  1079 
  1080 * Quickcheck:
  1081   - Added "eval" option to evaluate terms for the found counterexample
  1082     (currently only supported by the default (exhaustive) tester).
  1083   - Added post-processing of terms to obtain readable counterexamples
  1084     (currently only supported by the default (exhaustive) tester).
  1085   - New counterexample generator quickcheck[narrowing] enables
  1086     narrowing-based testing.  Requires the Glasgow Haskell compiler
  1087     with its installation location defined in the Isabelle settings
  1088     environment as ISABELLE_GHC.
  1089   - Removed quickcheck tester "SML" based on the SML code generator
  1090     (formly in HOL/Library).
  1091 
  1092 * Function package: discontinued option "tailrec".  INCOMPATIBILITY,
  1093 use 'partial_function' instead.
  1094 
  1095 * Theory Library/Extended_Reals replaces now the positive extended
  1096 reals found in probability theory. This file is extended by
  1097 Multivariate_Analysis/Extended_Real_Limits.
  1098 
  1099 * Theory Library/Old_Recdef: old 'recdef' package has been moved here,
  1100 from where it must be imported explicitly if it is really required.
  1101 INCOMPATIBILITY.
  1102 
  1103 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has
  1104 been moved here.  INCOMPATIBILITY.
  1105 
  1106 * Theory Library/Saturated provides type of numbers with saturated
  1107 arithmetic.
  1108 
  1109 * Theory Library/Product_Lattice defines a pointwise ordering for the
  1110 product type 'a * 'b, and provides instance proofs for various order
  1111 and lattice type classes.
  1112 
  1113 * Theory Library/Countable now provides the "countable_datatype" proof
  1114 method for proving "countable" class instances for datatypes.
  1115 
  1116 * Theory Library/Cset_Monad allows do notation for computable sets
  1117 (cset) via the generic monad ad-hoc overloading facility.
  1118 
  1119 * Library: Theories of common data structures are split into theories
  1120 for implementation, an invariant-ensuring type, and connection to an
  1121 abstract type. INCOMPATIBILITY.
  1122 
  1123   - RBT is split into RBT and RBT_Mapping.
  1124   - AssocList is split and renamed into AList and AList_Mapping.
  1125   - DList is split into DList_Impl, DList, and DList_Cset.
  1126   - Cset is split into Cset and List_Cset.
  1127 
  1128 * Theory Library/Nat_Infinity has been renamed to
  1129 Library/Extended_Nat, with name changes of the following types and
  1130 constants:
  1131 
  1132   type inat   ~> type enat
  1133   Fin         ~> enat
  1134   Infty       ~> infinity (overloaded)
  1135   iSuc        ~> eSuc
  1136   the_Fin     ~> the_enat
  1137 
  1138 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
  1139 been renamed accordingly. INCOMPATIBILITY.
  1140 
  1141 * Session Multivariate_Analysis: The euclidean_space type class now
  1142 fixes a constant "Basis :: 'a set" consisting of the standard
  1143 orthonormal basis for the type. Users now have the option of
  1144 quantifying over this set instead of using the "basis" function, e.g.
  1145 "ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".
  1146 
  1147 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
  1148 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants
  1149 "Cart_nth" and "Cart_lambda" have been respectively renamed to
  1150 "vec_nth" and "vec_lambda"; theorems mentioning those names have
  1151 changed to match. Definition theorems for overloaded constants now use
  1152 the standard "foo_vec_def" naming scheme. A few other theorems have
  1153 been renamed as follows (INCOMPATIBILITY):
  1154 
  1155   Cart_eq          ~> vec_eq_iff
  1156   dist_nth_le_cart ~> dist_vec_nth_le
  1157   tendsto_vector   ~> vec_tendstoI
  1158   Cauchy_vector    ~> vec_CauchyI
  1159 
  1160 * Session Multivariate_Analysis: Several duplicate theorems have been
  1161 removed, and other theorems have been renamed or replaced with more
  1162 general versions. INCOMPATIBILITY.
  1163 
  1164   finite_choice ~> finite_set_choice
  1165   eventually_conjI ~> eventually_conj
  1166   eventually_and ~> eventually_conj_iff
  1167   eventually_false ~> eventually_False
  1168   setsum_norm ~> norm_setsum
  1169   Lim_sequentially ~> LIMSEQ_def
  1170   Lim_ident_at ~> LIM_ident
  1171   Lim_const ~> tendsto_const
  1172   Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
  1173   Lim_neg ~> tendsto_minus
  1174   Lim_add ~> tendsto_add
  1175   Lim_sub ~> tendsto_diff
  1176   Lim_mul ~> tendsto_scaleR
  1177   Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
  1178   Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
  1179   Lim_linear ~> bounded_linear.tendsto
  1180   Lim_component ~> tendsto_euclidean_component
  1181   Lim_component_cart ~> tendsto_vec_nth
  1182   Lim_inner ~> tendsto_inner [OF tendsto_const]
  1183   dot_lsum ~> inner_setsum_left
  1184   dot_rsum ~> inner_setsum_right
  1185   continuous_cmul ~> continuous_scaleR [OF continuous_const]
  1186   continuous_neg ~> continuous_minus
  1187   continuous_sub ~> continuous_diff
  1188   continuous_vmul ~> continuous_scaleR [OF _ continuous_const]
  1189   continuous_mul ~> continuous_scaleR
  1190   continuous_inv ~> continuous_inverse
  1191   continuous_at_within_inv ~> continuous_at_within_inverse
  1192   continuous_at_inv ~> continuous_at_inverse
  1193   continuous_at_norm ~> continuous_norm [OF continuous_at_id]
  1194   continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]
  1195   continuous_at_component ~> continuous_component [OF continuous_at_id]
  1196   continuous_on_neg ~> continuous_on_minus
  1197   continuous_on_sub ~> continuous_on_diff
  1198   continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
  1199   continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
  1200   continuous_on_mul ~> continuous_on_scaleR
  1201   continuous_on_mul_real ~> continuous_on_mult
  1202   continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
  1203   continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]
  1204   continuous_on_inverse ~> continuous_on_inv
  1205   uniformly_continuous_on_neg ~> uniformly_continuous_on_minus
  1206   uniformly_continuous_on_sub ~> uniformly_continuous_on_diff
  1207   subset_interior ~> interior_mono
  1208   subset_closure ~> closure_mono
  1209   closure_univ ~> closure_UNIV
  1210   real_arch_lt ~> reals_Archimedean2
  1211   real_arch ~> reals_Archimedean3
  1212   real_abs_norm ~> abs_norm_cancel
  1213   real_abs_sub_norm ~> norm_triangle_ineq3
  1214   norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
  1215 
  1216 * Session HOL-Probability:
  1217   - Caratheodory's extension lemma is now proved for ring_of_sets.
  1218   - Infinite products of probability measures are now available.
  1219   - Sigma closure is independent, if the generator is independent
  1220   - Use extended reals instead of positive extended
  1221     reals. INCOMPATIBILITY.
  1222 
  1223 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.
  1224 
  1225   expand_fun_below ~> fun_below_iff
  1226   below_fun_ext ~> fun_belowI
  1227   expand_cfun_eq ~> cfun_eq_iff
  1228   ext_cfun ~> cfun_eqI
  1229   expand_cfun_below ~> cfun_below_iff
  1230   below_cfun_ext ~> cfun_belowI
  1231   monofun_fun_fun ~> fun_belowD
  1232   monofun_fun_arg ~> monofunE
  1233   monofun_lub_fun ~> adm_monofun [THEN admD]
  1234   cont_lub_fun ~> adm_cont [THEN admD]
  1235   cont2cont_Rep_CFun ~> cont2cont_APP
  1236   cont_Rep_CFun_app ~> cont_APP_app
  1237   cont_Rep_CFun_app_app ~> cont_APP_app_app
  1238   cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]
  1239   cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]
  1240   contlub_cfun ~> lub_APP [symmetric]
  1241   contlub_LAM ~> lub_LAM [symmetric]
  1242   thelubI ~> lub_eqI
  1243   UU_I ~> bottomI
  1244   lift_distinct1 ~> lift.distinct(1)
  1245   lift_distinct2 ~> lift.distinct(2)
  1246   Def_not_UU ~> lift.distinct(2)
  1247   Def_inject ~> lift.inject
  1248   below_UU_iff ~> below_bottom_iff
  1249   eq_UU_iff ~> eq_bottom_iff
  1250 
  1251 
  1252 *** Document preparation ***
  1253 
  1254 * Antiquotation @{rail} layouts railroad syntax diagrams, see also
  1255 isar-ref manual, both for description and actual application of the
  1256 same.
  1257 
  1258 * Antiquotation @{value} evaluates the given term and presents its
  1259 result.
  1260 
  1261 * Antiquotations: term style "isub" provides ad-hoc conversion of
  1262 variables x1, y23 into subscripted form x\<^isub>1,
  1263 y\<^isub>2\<^isub>3.
  1264 
  1265 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
  1266 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
  1267 
  1268 * Localized \isabellestyle switch can be used within blocks or groups
  1269 like this:
  1270 
  1271   \isabellestyle{it}  %preferred default
  1272   {\isabellestylett @{text "typewriter stuff"}}
  1273 
  1274 * Discontinued special treatment of hard tabulators.  Implicit
  1275 tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual
  1276 layouts.
  1277 
  1278 
  1279 *** ML ***
  1280 
  1281 * The inner syntax of sort/type/term/prop supports inlined YXML
  1282 representations within quoted string tokens.  By encoding logical
  1283 entities via Term_XML (in ML or Scala) concrete syntax can be
  1284 bypassed, which is particularly useful for producing bits of text
  1285 under external program control.
  1286 
  1287 * Antiquotations for ML and document preparation are managed as theory
  1288 data, which requires explicit setup.
  1289 
  1290 * Isabelle_Process.is_active allows tools to check if the official
  1291 process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
  1292 (better known as Proof General).
  1293 
  1294 * Structure Proof_Context follows standard naming scheme.  Old
  1295 ProofContext is still available for some time as legacy alias.
  1296 
  1297 * Structure Timing provides various operations for timing; supersedes
  1298 former start_timing/end_timing etc.
  1299 
  1300 * Path.print is the official way to show file-system paths to users
  1301 (including quotes etc.).
  1302 
  1303 * Inner syntax: identifiers in parse trees of generic categories
  1304 "logic", "aprop", "idt" etc. carry position information (disguised as
  1305 type constraints).  Occasional INCOMPATIBILITY with non-compliant
  1306 translations that choke on unexpected type constraints.  Positions can
  1307 be stripped in ML translations via Syntax.strip_positions /
  1308 Syntax.strip_positions_ast, or via the syntax constant
  1309 "_strip_positions" within parse trees.  As last resort, positions can
  1310 be disabled via the configuration option Syntax.positions, which is
  1311 called "syntax_positions" in Isar attribute syntax.
  1312 
  1313 * Discontinued special status of various ML structures that contribute
  1314 to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less
  1315 pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,
  1316 refer directly to Ast.Constant, Lexicon.is_identifier,
  1317 Syntax_Trans.mk_binder_tr etc.
  1318 
  1319 * Typed print translation: discontinued show_sorts argument, which is
  1320 already available via context of "advanced" translation.
  1321 
  1322 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
  1323 goal states; body tactic needs to address all subgoals uniformly.
  1324 
  1325 * Slightly more special eq_list/eq_set, with shortcut involving
  1326 pointer equality (assumes that eq relation is reflexive).
  1327 
  1328 * Classical tactics use proper Proof.context instead of historic types
  1329 claset/clasimpset.  Old-style declarations like addIs, addEs, addDs
  1330 operate directly on Proof.context.  Raw type claset retains its use as
  1331 snapshot of the classical context, which can be recovered via
  1332 (put_claset HOL_cs) etc.  Type clasimpset has been discontinued.
  1333 INCOMPATIBILITY, classical tactics and derived proof methods require
  1334 proper Proof.context.
  1335 
  1336 
  1337 *** System ***
  1338 
  1339 * Discontinued support for Poly/ML 5.2, which was the last version
  1340 without proper multithreading and TimeLimit implementation.
  1341 
  1342 * Discontinued old lib/scripts/polyml-platform, which has been
  1343 obsolete since Isabelle2009-2.
  1344 
  1345 * Various optional external tools are referenced more robustly and
  1346 uniformly by explicit Isabelle settings as follows:
  1347 
  1348   ISABELLE_CSDP   (formerly CSDP_EXE)
  1349   ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)
  1350   ISABELLE_OCAML  (formerly EXEC_OCAML)
  1351   ISABELLE_SWIPL  (formerly EXEC_SWIPL)
  1352   ISABELLE_YAP    (formerly EXEC_YAP)
  1353 
  1354 Note that automated detection from the file-system or search path has
  1355 been discontinued.  INCOMPATIBILITY.
  1356 
  1357 * Scala layer provides JVM method invocation service for static
  1358 methods of type (String)String, see Invoke_Scala.method in ML.  For
  1359 example:
  1360 
  1361   Invoke_Scala.method "java.lang.System.getProperty" "java.home"
  1362 
  1363 Together with YXML.string_of_body/parse_body and XML.Encode/Decode
  1364 this allows to pass structured values between ML and Scala.
  1365 
  1366 * The IsabelleText fonts includes some further glyphs to support the
  1367 Prover IDE.  Potential INCOMPATIBILITY: users who happen to have
  1368 installed a local copy (which is normally *not* required) need to
  1369 delete or update it from ~~/lib/fonts/.
  1370 
  1371 
  1372 
  1373 New in Isabelle2011 (January 2011)
  1374 ----------------------------------
  1375 
  1376 *** General ***
  1377 
  1378 * Experimental Prover IDE based on Isabelle/Scala and jEdit (see
  1379 src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with
  1380 useful tooltips and hyperlinks produced from its static analysis.  The
  1381 bundled component provides an executable Isabelle tool that can be run
  1382 like this:
  1383 
  1384   Isabelle2011/bin/isabelle jedit
  1385 
  1386 * Significantly improved Isabelle/Isar implementation manual.
  1387 
  1388 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
  1389 (and thus refers to something like $HOME/.isabelle/Isabelle2011),
  1390 while the default heap location within that directory lacks that extra
  1391 suffix.  This isolates multiple Isabelle installations from each
  1392 other, avoiding problems with old settings in new versions.
  1393 INCOMPATIBILITY, need to copy/upgrade old user settings manually.
  1394 
  1395 * Source files are always encoded as UTF-8, instead of old-fashioned
  1396 ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require
  1397 the following package declarations:
  1398 
  1399   \usepackage[utf8]{inputenc}
  1400   \usepackage{textcomp}
  1401 
  1402 * Explicit treatment of UTF-8 sequences as Isabelle symbols, such that
  1403 a Unicode character is treated as a single symbol, not a sequence of
  1404 non-ASCII bytes as before.  Since Isabelle/ML string literals may
  1405 contain symbols without further backslash escapes, Unicode can now be
  1406 used here as well.  Recall that Symbol.explode in ML provides a
  1407 consistent view on symbols, while raw explode (or String.explode)
  1408 merely give a byte-oriented representation.
  1409 
  1410 * Theory loader: source files are primarily located via the master
  1411 directory of each theory node (where the .thy file itself resides).
  1412 The global load path is still partially available as legacy feature.
  1413 Minor INCOMPATIBILITY due to subtle change in file lookup: use
  1414 explicit paths, relatively to the theory.
  1415 
  1416 * Special treatment of ML file names has been discontinued.
  1417 Historically, optional extensions .ML or .sml were added on demand --
  1418 at the cost of clarity of file dependencies.  Recall that Isabelle/ML
  1419 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
  1420 
  1421 * Various options that affect pretty printing etc. are now properly
  1422 handled within the context via configuration options, instead of
  1423 unsynchronized references or print modes.  There are both ML Config.T
  1424 entities and Isar declaration attributes to access these.
  1425 
  1426   ML (Config.T)                 Isar (attribute)
  1427 
  1428   eta_contract                  eta_contract
  1429   show_brackets                 show_brackets
  1430   show_sorts                    show_sorts
  1431   show_types                    show_types
  1432   show_question_marks           show_question_marks
  1433   show_consts                   show_consts
  1434   show_abbrevs                  show_abbrevs
  1435 
  1436   Syntax.ast_trace              syntax_ast_trace
  1437   Syntax.ast_stat               syntax_ast_stat
  1438   Syntax.ambiguity_level        syntax_ambiguity_level
  1439 
  1440   Goal_Display.goals_limit      goals_limit
  1441   Goal_Display.show_main_goal   show_main_goal
  1442 
  1443   Method.rule_trace             rule_trace
  1444 
  1445   Thy_Output.display            thy_output_display
  1446   Thy_Output.quotes             thy_output_quotes
  1447   Thy_Output.indent             thy_output_indent
  1448   Thy_Output.source             thy_output_source
  1449   Thy_Output.break              thy_output_break
  1450 
  1451 Note that corresponding "..._default" references in ML may only be
  1452 changed globally at the ROOT session setup, but *not* within a theory.
  1453 The option "show_abbrevs" supersedes the former print mode
  1454 "no_abbrevs" with inverted meaning.
  1455 
  1456 * More systematic naming of some configuration options.
  1457 INCOMPATIBILITY.
  1458 
  1459   trace_simp  ~>  simp_trace
  1460   debug_simp  ~>  simp_debug
  1461 
  1462 * Support for real valued configuration options, using simplistic
  1463 floating-point notation that coincides with the inner syntax for
  1464 float_token.
  1465 
  1466 * Support for real valued preferences (with approximative PGIP type):
  1467 front-ends need to accept "pgint" values in float notation.
  1468 INCOMPATIBILITY.
  1469 
  1470 * The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
  1471 DejaVu Sans.
  1472 
  1473 * Discontinued support for Poly/ML 5.0 and 5.1 versions.
  1474 
  1475 
  1476 *** Pure ***
  1477 
  1478 * Command 'type_synonym' (with single argument) replaces somewhat
  1479 outdated 'types', which is still available as legacy feature for some
  1480 time.
  1481 
  1482 * Command 'nonterminal' (with 'and' separated list of arguments)
  1483 replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.
  1484 
  1485 * Command 'notepad' replaces former 'example_proof' for
  1486 experimentation in Isar without any result.  INCOMPATIBILITY.
  1487 
  1488 * Locale interpretation commands 'interpret' and 'sublocale' accept
  1489 lists of equations to map definitions in a locale to appropriate
  1490 entities in the context of the interpretation.  The 'interpretation'
  1491 command already provided this functionality.
  1492 
  1493 * Diagnostic command 'print_dependencies' prints the locale instances
  1494 that would be activated if the specified expression was interpreted in
  1495 the current context.  Variant "print_dependencies!" assumes a context
  1496 without interpretations.
  1497 
  1498 * Diagnostic command 'print_interps' prints interpretations in proofs
  1499 in addition to interpretations in theories.
  1500 
  1501 * Discontinued obsolete 'global' and 'local' commands to manipulate
  1502 the theory name space.  Rare INCOMPATIBILITY.  The ML functions
  1503 Sign.root_path and Sign.local_path may be applied directly where this
  1504 feature is still required for historical reasons.
  1505 
  1506 * Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use
  1507 'definition' instead.
  1508 
  1509 * The "prems" fact, which refers to the accidental collection of
  1510 foundational premises in the context, is now explicitly marked as
  1511 legacy feature and will be discontinued soon.  Consider using "assms"
  1512 of the head statement or reference facts by explicit names.
  1513 
  1514 * Document antiquotations @{class} and @{type} print classes and type
  1515 constructors.
  1516 
  1517 * Document antiquotation @{file} checks file/directory entries within
  1518 the local file system.
  1519 
  1520 
  1521 *** HOL ***
  1522 
  1523 * Coercive subtyping: functions can be declared as coercions and type
  1524 inference will add them as necessary upon input of a term.  Theory
  1525 Complex_Main declares real :: nat => real and real :: int => real as
  1526 coercions. A coercion function f is declared like this:
  1527 
  1528   declare [[coercion f]]
  1529 
  1530 To lift coercions through type constructors (e.g. from nat => real to
  1531 nat list => real list), map functions can be declared, e.g.
  1532 
  1533   declare [[coercion_map map]]
  1534 
  1535 Currently coercion inference is activated only in theories including
  1536 real numbers, i.e. descendants of Complex_Main.  This is controlled by
  1537 the configuration option "coercion_enabled", e.g. it can be enabled in
  1538 other theories like this:
  1539 
  1540   declare [[coercion_enabled]]
  1541 
  1542 * Command 'partial_function' provides basic support for recursive
  1543 function definitions over complete partial orders.  Concrete instances
  1544 are provided for i) the option type, ii) tail recursion on arbitrary
  1545 types, and iii) the heap monad of Imperative_HOL.  See
  1546 src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy
  1547 for examples.
  1548 
  1549 * Function package: f.psimps rules are no longer implicitly declared
  1550 as [simp].  INCOMPATIBILITY.
  1551 
  1552 * Datatype package: theorems generated for executable equality (class
  1553 "eq") carry proper names and are treated as default code equations.
  1554 
  1555 * Inductive package: now offers command 'inductive_simps' to
  1556 automatically derive instantiated and simplified equations for
  1557 inductive predicates, similar to 'inductive_cases'.
  1558 
  1559 * Command 'enriched_type' allows to register properties of the
  1560 functorial structure of types.
  1561 
  1562 * Improved infrastructure for term evaluation using code generator
  1563 techniques, in particular static evaluation conversions.
  1564 
  1565 * Code generator: Scala (2.8 or higher) has been added to the target
  1566 languages.
  1567 
  1568 * Code generator: globbing constant expressions "*" and "Theory.*"
  1569 have been replaced by the more idiomatic "_" and "Theory._".
  1570 INCOMPATIBILITY.
  1571 
  1572 * Code generator: export_code without explicit file declaration prints
  1573 to standard output.  INCOMPATIBILITY.
  1574 
  1575 * Code generator: do not print function definitions for case
  1576 combinators any longer.
  1577 
  1578 * Code generator: simplification with rules determined with
  1579 src/Tools/Code/code_simp.ML and method "code_simp".
  1580 
  1581 * Code generator for records: more idiomatic representation of record
  1582 types.  Warning: records are not covered by ancient SML code
  1583 generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable
  1584 rep_datatype declaration helps to succeed then:
  1585 
  1586   record 'a foo = ...
  1587   ...
  1588   rep_datatype foo_ext ...
  1589 
  1590 * Records: logical foundation type for records does not carry a
  1591 '_type' suffix any longer (obsolete due to authentic syntax).
  1592 INCOMPATIBILITY.
  1593 
  1594 * Quickcheck now by default uses exhaustive testing instead of random
  1595 testing.  Random testing can be invoked by "quickcheck [random]",
  1596 exhaustive testing by "quickcheck [exhaustive]".
  1597 
  1598 * Quickcheck instantiates polymorphic types with small finite
  1599 datatypes by default. This enables a simple execution mechanism to
  1600 handle quantifiers and function equality over the finite datatypes.
  1601 
  1602 * Quickcheck random generator has been renamed from "code" to
  1603 "random".  INCOMPATIBILITY.
  1604 
  1605 * Quickcheck now has a configurable time limit which is set to 30
  1606 seconds by default. This can be changed by adding [timeout = n] to the
  1607 quickcheck command. The time limit for Auto Quickcheck is still set
  1608 independently.
  1609 
  1610 * Quickcheck in locales considers interpretations of that locale for
  1611 counter example search.
  1612 
  1613 * Sledgehammer:
  1614   - Added "smt" and "remote_smt" provers based on the "smt" proof
  1615     method. See the Sledgehammer manual for details ("isabelle doc
  1616     sledgehammer").
  1617   - Renamed commands:
  1618     sledgehammer atp_info ~> sledgehammer running_provers
  1619     sledgehammer atp_kill ~> sledgehammer kill_provers
  1620     sledgehammer available_atps ~> sledgehammer available_provers
  1621     INCOMPATIBILITY.
  1622   - Renamed options:
  1623     sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
  1624     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
  1625     sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
  1626     (and "ms" and "min" are no longer supported)
  1627     INCOMPATIBILITY.
  1628 
  1629 * Nitpick:
  1630   - Renamed options:
  1631     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
  1632     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
  1633     INCOMPATIBILITY.
  1634   - Added support for partial quotient types.
  1635   - Added local versions of the "Nitpick.register_xxx" functions.
  1636   - Added "whack" option.
  1637   - Allow registration of quotient types as codatatypes.
  1638   - Improved "merge_type_vars" option to merge more types.
  1639   - Removed unsound "fast_descrs" option.
  1640   - Added custom symmetry breaking for datatypes, making it possible to reach
  1641     higher cardinalities.
  1642   - Prevent the expansion of too large definitions.
  1643 
  1644 * Proof methods "metis" and "meson" now have configuration options
  1645 "meson_trace", "metis_trace", and "metis_verbose" that can be enabled
  1646 to diagnose these tools. E.g.
  1647 
  1648     using [[metis_trace = true]]
  1649 
  1650 * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
  1651 manually as command 'solve_direct'.
  1652 
  1653 * The default SMT solver Z3 must be enabled explicitly (due to
  1654 licensing issues) by setting the environment variable
  1655 Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For
  1656 commercial applications, the SMT solver CVC3 is provided as fall-back;
  1657 changing the SMT solver is done via the configuration option
  1658 "smt_solver".
  1659 
  1660 * Remote SMT solvers need to be referred to by the "remote_" prefix,
  1661 i.e. "remote_cvc3" and "remote_z3".
  1662 
  1663 * Added basic SMT support for datatypes, records, and typedefs using
  1664 the oracle mode (no proofs).  Direct support of pairs has been dropped
  1665 in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT
  1666 support for a similar behavior).  Minor INCOMPATIBILITY.
  1667 
  1668 * Changed SMT configuration options:
  1669   - Renamed:
  1670     z3_proofs ~> smt_oracle (with inverted meaning)
  1671     z3_trace_assms ~> smt_trace_used_facts
  1672     INCOMPATIBILITY.
  1673   - Added:
  1674     smt_verbose
  1675     smt_random_seed
  1676     smt_datatypes
  1677     smt_infer_triggers
  1678     smt_monomorph_limit
  1679     cvc3_options
  1680     remote_cvc3_options
  1681     remote_z3_options
  1682     yices_options
  1683 
  1684 * Boogie output files (.b2i files) need to be declared in the theory
  1685 header.
  1686 
  1687 * Simplification procedure "list_to_set_comprehension" rewrites list
  1688 comprehensions applied to List.set to set comprehensions.  Occasional
  1689 INCOMPATIBILITY, may be deactivated like this:
  1690 
  1691   declare [[simproc del: list_to_set_comprehension]]
  1692 
  1693 * Removed old version of primrec package.  INCOMPATIBILITY.
  1694 
  1695 * Removed simplifier congruence rule of "prod_case", as has for long
  1696 been the case with "split".  INCOMPATIBILITY.
  1697 
  1698 * String.literal is a type, but not a datatype.  INCOMPATIBILITY.
  1699 
  1700 * Removed [split_format ... and ... and ...] version of
  1701 [split_format].  Potential INCOMPATIBILITY.
  1702 
  1703 * Predicate "sorted" now defined inductively, with nice induction
  1704 rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.
  1705 
  1706 * Constant "contents" renamed to "the_elem", to free the generic name
  1707 contents for other uses.  INCOMPATIBILITY.
  1708 
  1709 * Renamed class eq and constant eq (for code generation) to class
  1710 equal and constant equal, plus renaming of related facts and various
  1711 tuning.  INCOMPATIBILITY.
  1712 
  1713 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
  1714 
  1715 * Removed output syntax "'a ~=> 'b" for "'a => 'b option".
  1716 INCOMPATIBILITY.
  1717 
  1718 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
  1719 avoid confusion with finite sets.  INCOMPATIBILITY.
  1720 
  1721 * Abandoned locales equiv, congruent and congruent2 for equivalence
  1722 relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same
  1723 for congruent(2)).
  1724 
  1725 * Some previously unqualified names have been qualified:
  1726 
  1727   types
  1728     bool ~> HOL.bool
  1729     nat ~> Nat.nat
  1730 
  1731   constants
  1732     Trueprop ~> HOL.Trueprop
  1733     True ~> HOL.True
  1734     False ~> HOL.False
  1735     op & ~> HOL.conj
  1736     op | ~> HOL.disj
  1737     op --> ~> HOL.implies
  1738     op = ~> HOL.eq
  1739     Not ~> HOL.Not
  1740     The ~> HOL.The
  1741     All ~> HOL.All
  1742     Ex ~> HOL.Ex
  1743     Ex1 ~> HOL.Ex1
  1744     Let ~> HOL.Let
  1745     If ~> HOL.If
  1746     Ball ~> Set.Ball
  1747     Bex ~> Set.Bex
  1748     Suc ~> Nat.Suc
  1749     Pair ~> Product_Type.Pair
  1750     fst ~> Product_Type.fst
  1751     snd ~> Product_Type.snd
  1752     curry ~> Product_Type.curry
  1753     op : ~> Set.member
  1754     Collect ~> Set.Collect
  1755 
  1756 INCOMPATIBILITY.
  1757 
  1758 * More canonical naming convention for some fundamental definitions:
  1759 
  1760     bot_bool_eq ~> bot_bool_def
  1761     top_bool_eq ~> top_bool_def
  1762     inf_bool_eq ~> inf_bool_def
  1763     sup_bool_eq ~> sup_bool_def
  1764     bot_fun_eq  ~> bot_fun_def
  1765     top_fun_eq  ~> top_fun_def
  1766     inf_fun_eq  ~> inf_fun_def
  1767     sup_fun_eq  ~> sup_fun_def
  1768 
  1769 INCOMPATIBILITY.
  1770 
  1771 * More stylized fact names:
  1772 
  1773   expand_fun_eq ~> fun_eq_iff
  1774   expand_set_eq ~> set_eq_iff
  1775   set_ext       ~> set_eqI
  1776   nat_number    ~> eval_nat_numeral
  1777 
  1778 INCOMPATIBILITY.
  1779 
  1780 * Refactoring of code-generation specific operations in theory List:
  1781 
  1782   constants
  1783     null ~> List.null
  1784 
  1785   facts
  1786     mem_iff ~> member_def
  1787     null_empty ~> null_def
  1788 
  1789 INCOMPATIBILITY.  Note that these were not supposed to be used
  1790 regularly unless for striking reasons; their main purpose was code
  1791 generation.
  1792 
  1793 Various operations from the Haskell prelude are used for generating
  1794 Haskell code.
  1795 
  1796 * Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV".  Term
  1797 "surj f" is now an abbreviation of "range f = UNIV".  The theorems
  1798 bij_def and surj_def are unchanged.  INCOMPATIBILITY.
  1799 
  1800 * Abolished some non-alphabetic type names: "prod" and "sum" replace
  1801 "*" and "+" respectively.  INCOMPATIBILITY.
  1802 
  1803 * Name "Plus" of disjoint sum operator "<+>" is now hidden.  Write
  1804 "Sum_Type.Plus" instead.
  1805 
  1806 * Constant "split" has been merged with constant "prod_case"; names of
  1807 ML functions, facts etc. involving split have been retained so far,
  1808 though.  INCOMPATIBILITY.
  1809 
  1810 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"
  1811 instead.  INCOMPATIBILITY.
  1812 
  1813 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".
  1814 INCOMPATIBILITY.
  1815 
  1816 * Former theory Library/Enum is now part of the HOL-Main image.
  1817 INCOMPATIBILITY: all constants of the Enum theory now have to be
  1818 referred to by its qualified name.
  1819 
  1820   enum    ~>  Enum.enum
  1821   nlists  ~>  Enum.nlists
  1822   product ~>  Enum.product
  1823 
  1824 * Theory Library/Monad_Syntax provides do-syntax for monad types.
  1825 Syntax in Library/State_Monad has been changed to avoid ambiguities.
  1826 INCOMPATIBILITY.
  1827 
  1828 * Theory Library/SetsAndFunctions has been split into
  1829 Library/Function_Algebras and Library/Set_Algebras; canonical names
  1830 for instance definitions for functions; various improvements.
  1831 INCOMPATIBILITY.
  1832 
  1833 * Theory Library/Multiset provides stable quicksort implementation of
  1834 sort_key.
  1835 
  1836 * Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
  1837 INCOMPATIBILITY.
  1838 
  1839 * Session Multivariate_Analysis: introduced a type class for euclidean
  1840 space.  Most theorems are now stated in terms of euclidean spaces
  1841 instead of finite cartesian products.
  1842 
  1843   types
  1844     real ^ 'n ~>  'a::real_vector
  1845               ~>  'a::euclidean_space
  1846               ~>  'a::ordered_euclidean_space
  1847         (depends on your needs)
  1848 
  1849   constants
  1850      _ $ _        ~> _ $$ _
  1851      \<chi> x. _  ~> \<chi>\<chi> x. _
  1852      CARD('n)     ~> DIM('a)
  1853 
  1854 Also note that the indices are now natural numbers and not from some
  1855 finite type. Finite cartesian products of euclidean spaces, products
  1856 of euclidean spaces the real and complex numbers are instantiated to
  1857 be euclidean_spaces.  INCOMPATIBILITY.
  1858 
  1859 * Session Probability: introduced pextreal as positive extended real
  1860 numbers.  Use pextreal as value for measures.  Introduce the
  1861 Radon-Nikodym derivative, product spaces and Fubini's theorem for
  1862 arbitrary sigma finite measures.  Introduces Lebesgue measure based on
  1863 the integral in Multivariate Analysis.  INCOMPATIBILITY.
  1864 
  1865 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.
  1866 INCOMPATIBILITY.
  1867 
  1868 * Session SPARK (with image HOL-SPARK) provides commands to load and
  1869 prove verification conditions generated by the SPARK Ada program
  1870 verifier.  See also src/HOL/SPARK and src/HOL/SPARK/Examples.
  1871 
  1872 
  1873 *** HOL-Algebra ***
  1874 
  1875 * Theorems for additive ring operations (locale abelian_monoid and
  1876 descendants) are generated by interpretation from their multiplicative
  1877 counterparts.  Names (in particular theorem names) have the mandatory
  1878 qualifier 'add'.  Previous theorem names are redeclared for
  1879 compatibility.
  1880 
  1881 * Structure "int_ring" is now an abbreviation (previously a
  1882 definition).  This fits more natural with advanced interpretations.
  1883 
  1884 
  1885 *** HOLCF ***
  1886 
  1887 * The domain package now runs in definitional mode by default: The
  1888 former command 'new_domain' is now called 'domain'.  To use the domain
  1889 package in its original axiomatic mode, use 'domain (unsafe)'.
  1890 INCOMPATIBILITY.
  1891 
  1892 * The new class "domain" is now the default sort.  Class "predomain"
  1893 is an unpointed version of "domain". Theories can be updated by
  1894 replacing sort annotations as shown below.  INCOMPATIBILITY.
  1895 
  1896   'a::type ~> 'a::countable
  1897   'a::cpo  ~> 'a::predomain
  1898   'a::pcpo ~> 'a::domain
  1899 
  1900 * The old type class "rep" has been superseded by class "domain".
  1901 Accordingly, users of the definitional package must remove any
  1902 "default_sort rep" declarations.  INCOMPATIBILITY.
  1903 
  1904 * The domain package (definitional mode) now supports unpointed
  1905 predomain argument types, as long as they are marked 'lazy'. (Strict
  1906 arguments must be in class "domain".) For example, the following
  1907 domain definition now works:
  1908 
  1909   domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")
  1910 
  1911 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class
  1912 instances for types from main HOL: bool, nat, int, char, 'a + 'b,
  1913 'a option, and 'a list.  Additionally, it configures fixrec and the
  1914 domain package to work with these types.  For example:
  1915 
  1916   fixrec isInl :: "('a + 'b) u -> tr"
  1917     where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"
  1918 
  1919   domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")
  1920 
  1921 * The "(permissive)" option of fixrec has been replaced with a
  1922 per-equation "(unchecked)" option. See
  1923 src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.
  1924 
  1925 * The "bifinite" class no longer fixes a constant "approx"; the class
  1926 now just asserts that such a function exists.  INCOMPATIBILITY.
  1927 
  1928 * Former type "alg_defl" has been renamed to "defl".  HOLCF no longer
  1929 defines an embedding of type 'a defl into udom by default; instances
  1930 of "bifinite" and "domain" classes are available in
  1931 src/HOL/HOLCF/Library/Defl_Bifinite.thy.
  1932 
  1933 * The syntax "REP('a)" has been replaced with "DEFL('a)".
  1934 
  1935 * The predicate "directed" has been removed.  INCOMPATIBILITY.
  1936 
  1937 * The type class "finite_po" has been removed.  INCOMPATIBILITY.
  1938 
  1939 * The function "cprod_map" has been renamed to "prod_map".
  1940 INCOMPATIBILITY.
  1941 
  1942 * The monadic bind operator on each powerdomain has new binder syntax
  1943 similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents
  1944 "upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".
  1945 
  1946 * The infix syntax for binary union on each powerdomain has changed
  1947 from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set
  1948 syntax.  INCOMPATIBILITY.
  1949 
  1950 * The constant "UU" has been renamed to "bottom".  The syntax "UU" is
  1951 still supported as an input translation.
  1952 
  1953 * Renamed some theorems (the original names are also still available).
  1954 
  1955   expand_fun_below   ~> fun_below_iff
  1956   below_fun_ext      ~> fun_belowI
  1957   expand_cfun_eq     ~> cfun_eq_iff
  1958   ext_cfun           ~> cfun_eqI
  1959   expand_cfun_below  ~> cfun_below_iff
  1960   below_cfun_ext     ~> cfun_belowI
  1961   cont2cont_Rep_CFun ~> cont2cont_APP
  1962 
  1963 * The Abs and Rep functions for various types have changed names.
  1964 Related theorem names have also changed to match. INCOMPATIBILITY.
  1965 
  1966   Rep_CFun  ~> Rep_cfun
  1967   Abs_CFun  ~> Abs_cfun
  1968   Rep_Sprod ~> Rep_sprod
  1969   Abs_Sprod ~> Abs_sprod
  1970   Rep_Ssum  ~> Rep_ssum
  1971   Abs_Ssum  ~> Abs_ssum
  1972 
  1973 * Lemmas with names of the form *_defined_iff or *_strict_iff have
  1974 been renamed to *_bottom_iff.  INCOMPATIBILITY.
  1975 
  1976 * Various changes to bisimulation/coinduction with domain package:
  1977 
  1978   - Definitions of "bisim" constants no longer mention definedness.
  1979   - With mutual recursion, "bisim" predicate is now curried.
  1980   - With mutual recursion, each type gets a separate coind theorem.
  1981   - Variable names in bisim_def and coinduct rules have changed.
  1982 
  1983 INCOMPATIBILITY.
  1984 
  1985 * Case combinators generated by the domain package for type "foo" are
  1986 now named "foo_case" instead of "foo_when".  INCOMPATIBILITY.
  1987 
  1988 * Several theorems have been renamed to more accurately reflect the
  1989 names of constants and types involved.  INCOMPATIBILITY.
  1990 
  1991   thelub_const    ~> lub_const
  1992   lub_const       ~> is_lub_const
  1993   thelubI         ~> lub_eqI
  1994   is_lub_lub      ~> is_lubD2
  1995   lubI            ~> is_lub_lub
  1996   unique_lub      ~> is_lub_unique
  1997   is_ub_lub       ~> is_lub_rangeD1
  1998   lub_bin_chain   ~> is_lub_bin_chain
  1999   lub_fun         ~> is_lub_fun
  2000   thelub_fun      ~> lub_fun
  2001   thelub_cfun     ~> lub_cfun
  2002   thelub_Pair     ~> lub_Pair
  2003   lub_cprod       ~> is_lub_prod
  2004   thelub_cprod    ~> lub_prod
  2005   minimal_cprod   ~> minimal_prod
  2006   inst_cprod_pcpo ~> inst_prod_pcpo
  2007   UU_I            ~> bottomI
  2008   compact_UU      ~> compact_bottom
  2009   deflation_UU    ~> deflation_bottom
  2010   finite_deflation_UU ~> finite_deflation_bottom
  2011 
  2012 * Many legacy theorem names have been discontinued.  INCOMPATIBILITY.
  2013 
  2014   sq_ord_less_eq_trans ~> below_eq_trans
  2015   sq_ord_eq_less_trans ~> eq_below_trans
  2016   refl_less            ~> below_refl
  2017   trans_less           ~> below_trans
  2018   antisym_less         ~> below_antisym
  2019   antisym_less_inverse ~> po_eq_conv [THEN iffD1]
  2020   box_less             ~> box_below
  2021   rev_trans_less       ~> rev_below_trans
  2022   not_less2not_eq      ~> not_below2not_eq
  2023   less_UU_iff          ~> below_UU_iff
  2024   flat_less_iff        ~> flat_below_iff
  2025   adm_less             ~> adm_below
  2026   adm_not_less         ~> adm_not_below
  2027   adm_compact_not_less ~> adm_compact_not_below
  2028   less_fun_def         ~> below_fun_def
  2029   expand_fun_less      ~> fun_below_iff
  2030   less_fun_ext         ~> fun_belowI
  2031   less_discr_def       ~> below_discr_def
  2032   discr_less_eq        ~> discr_below_eq
  2033   less_unit_def        ~> below_unit_def
  2034   less_cprod_def       ~> below_prod_def
  2035   prod_lessI           ~> prod_belowI
  2036   Pair_less_iff        ~> Pair_below_iff
  2037   fst_less_iff         ~> fst_below_iff
  2038   snd_less_iff         ~> snd_below_iff
  2039   expand_cfun_less     ~> cfun_below_iff
  2040   less_cfun_ext        ~> cfun_belowI
  2041   injection_less       ~> injection_below
  2042   less_up_def          ~> below_up_def
  2043   not_Iup_less         ~> not_Iup_below
  2044   Iup_less             ~> Iup_below
  2045   up_less              ~> up_below
  2046   Def_inject_less_eq   ~> Def_below_Def
  2047   Def_less_is_eq       ~> Def_below_iff
  2048   spair_less_iff       ~> spair_below_iff
  2049   less_sprod           ~> below_sprod
  2050   spair_less           ~> spair_below
  2051   sfst_less_iff        ~> sfst_below_iff
  2052   ssnd_less_iff        ~> ssnd_below_iff
  2053   fix_least_less       ~> fix_least_below
  2054   dist_less_one        ~> dist_below_one
  2055   less_ONE             ~> below_ONE
  2056   ONE_less_iff         ~> ONE_below_iff
  2057   less_sinlD           ~> below_sinlD
  2058   less_sinrD           ~> below_sinrD
  2059 
  2060 
  2061 *** FOL and ZF ***
  2062 
  2063 * All constant names are now qualified internally and use proper
  2064 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
  2065 
  2066 
  2067 *** ML ***
  2068 
  2069 * Antiquotation @{assert} inlines a function bool -> unit that raises
  2070 Fail if the argument is false.  Due to inlining the source position of
  2071 failed assertions is included in the error output.
  2072 
  2073 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML
  2074 text is in practice always evaluated with a stable theory checkpoint.
  2075 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
  2076 
  2077 * Antiquotation @{theory A} refers to theory A from the ancestry of
  2078 the current context, not any accidental theory loader state as before.
  2079 Potential INCOMPATIBILITY, subtle change in semantics.
  2080 
  2081 * Syntax.pretty_priority (default 0) configures the required priority
  2082 of pretty-printed output and thus affects insertion of parentheses.
  2083 
  2084 * Syntax.default_root (default "any") configures the inner syntax
  2085 category (nonterminal symbol) for parsing of terms.
  2086 
  2087 * Former exception Library.UnequalLengths now coincides with
  2088 ListPair.UnequalLengths.
  2089 
  2090 * Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the
  2091 main functionality is provided by structure Simplifier.
  2092 
  2093 * Renamed raw "explode" function to "raw_explode" to emphasize its
  2094 meaning.  Note that internally to Isabelle, Symbol.explode is used in
  2095 almost all situations.
  2096 
  2097 * Discontinued obsolete function sys_error and exception SYS_ERROR.
  2098 See implementation manual for further details on exceptions in
  2099 Isabelle/ML.
  2100 
  2101 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
  2102 meaning.
  2103 
  2104 * Renamed structure PureThy to Pure_Thy and moved most of its
  2105 operations to structure Global_Theory, to emphasize that this is
  2106 rarely-used global-only stuff.
  2107 
  2108 * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
  2109 instead (or tracing for high-volume output).
  2110 
  2111 * Configuration option show_question_marks only affects regular pretty
  2112 printing of types and terms, not raw Term.string_of_vname.
  2113 
  2114 * ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
  2115 INCOMPATIBILITY, superseded by static antiquotations @{thm} and
  2116 @{thms} for most purposes.
  2117 
  2118 * ML structure Unsynchronized is never opened, not even in Isar
  2119 interaction mode as before.  Old Unsynchronized.set etc. have been
  2120 discontinued -- use plain := instead.  This should be *rare* anyway,
  2121 since modern tools always work via official context data, notably
  2122 configuration options.
  2123 
  2124 * Parallel and asynchronous execution requires special care concerning
  2125 interrupts.  Structure Exn provides some convenience functions that
  2126 avoid working directly with raw Interrupt.  User code must not absorb
  2127 interrupts -- intermediate handling (for cleanup etc.) needs to be
  2128 followed by re-raising of the original exception.  Another common
  2129 source of mistakes are "handle _" patterns, which make the meaning of
  2130 the program subject to physical effects of the environment.
  2131 
  2132 
  2133 
  2134 New in Isabelle2009-2 (June 2010)
  2135 ---------------------------------
  2136 
  2137 *** General ***
  2138 
  2139 * Authentic syntax for *all* logical entities (type classes, type
  2140 constructors, term constants): provides simple and robust
  2141 correspondence between formal entities and concrete syntax.  Within
  2142 the parse tree / AST representations, "constants" are decorated by
  2143 their category (class, type, const) and spelled out explicitly with
  2144 their full internal name.
  2145 
  2146 Substantial INCOMPATIBILITY concerning low-level syntax declarations
  2147 and translations (translation rules and translation functions in ML).
  2148 Some hints on upgrading:
  2149 
  2150   - Many existing uses of 'syntax' and 'translations' can be replaced
  2151     by more modern 'type_notation', 'notation' and 'abbreviation',
  2152     which are independent of this issue.
  2153 
  2154   - 'translations' require markup within the AST; the term syntax
  2155     provides the following special forms:
  2156 
  2157       CONST c   -- produces syntax version of constant c from context
  2158       XCONST c  -- literally c, checked as constant from context
  2159       c         -- literally c, if declared by 'syntax'
  2160 
  2161     Plain identifiers are treated as AST variables -- occasionally the
  2162     system indicates accidental variables via the error "rhs contains
  2163     extra variables".
  2164 
  2165     Type classes and type constructors are marked according to their
  2166     concrete syntax.  Some old translations rules need to be written
  2167     for the "type" category, using type constructor application
  2168     instead of pseudo-term application of the default category
  2169     "logic".
  2170 
  2171   - 'parse_translation' etc. in ML may use the following
  2172     antiquotations:
  2173 
  2174       @{class_syntax c}   -- type class c within parse tree / AST
  2175       @{term_syntax c}    -- type constructor c within parse tree / AST
  2176       @{const_syntax c}   -- ML version of "CONST c" above
  2177       @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)
  2178 
  2179   - Literal types within 'typed_print_translations', i.e. those *not*
  2180     represented as pseudo-terms are represented verbatim.  Use @{class
  2181     c} or @{type_name c} here instead of the above syntax
  2182     antiquotations.
  2183 
  2184 Note that old non-authentic syntax was based on unqualified base
  2185 names, so all of the above "constant" names would coincide.  Recall
  2186 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
  2187 diagnose syntax problems.
  2188 
  2189 * Type constructors admit general mixfix syntax, not just infix.
  2190 
  2191 * Concrete syntax may be attached to local entities without a proof
  2192 body, too.  This works via regular mixfix annotations for 'fix',
  2193 'def', 'obtain' etc. or via the explicit 'write' command, which is
  2194 similar to the 'notation' command in theory specifications.
  2195 
  2196 * Discontinued unnamed infix syntax (legacy feature for many years) --
  2197 need to specify constant name and syntax separately.  Internal ML
  2198 datatype constructors have been renamed from InfixName to Infix etc.
  2199 Minor INCOMPATIBILITY.
  2200 
  2201 * Schematic theorem statements need to be explicitly markup as such,
  2202 via commands 'schematic_lemma', 'schematic_theorem',
  2203 'schematic_corollary'.  Thus the relevance of the proof is made
  2204 syntactically clear, which impacts performance in a parallel or
  2205 asynchronous interactive environment.  Minor INCOMPATIBILITY.
  2206 
  2207 * Use of cumulative prems via "!" in some proof methods has been
  2208 discontinued (old legacy feature).
  2209 
  2210 * References 'trace_simp' and 'debug_simp' have been replaced by
  2211 configuration options stored in the context. Enabling tracing (the
  2212 case of debugging is similar) in proofs works via
  2213 
  2214   using [[trace_simp = true]]
  2215 
  2216 Tracing is then active for all invocations of the simplifier in
  2217 subsequent goal refinement steps. Tracing may also still be enabled or
  2218 disabled via the ProofGeneral settings menu.
  2219 
  2220 * Separate commands 'hide_class', 'hide_type', 'hide_const',
  2221 'hide_fact' replace the former 'hide' KIND command.  Minor
  2222 INCOMPATIBILITY.
  2223 
  2224 * Improved parallelism of proof term normalization: usedir -p2 -q0 is
  2225 more efficient than combinations with -q1 or -q2.
  2226 
  2227 
  2228 *** Pure ***
  2229 
  2230 * Proofterms record type-class reasoning explicitly, using the
  2231 "unconstrain" operation internally.  This eliminates all sort
  2232 constraints from a theorem and proof, introducing explicit
  2233 OFCLASS-premises.  On the proof term level, this operation is
  2234 automatically applied at theorem boundaries, such that closed proofs
  2235 are always free of sort constraints.  INCOMPATIBILITY for tools that
  2236 inspect proof terms.
  2237 
  2238 * Local theory specifications may depend on extra type variables that
  2239 are not present in the result type -- arguments TYPE('a) :: 'a itself
  2240 are added internally.  For example:
  2241 
  2242   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
  2243 
  2244 * Predicates of locales introduced by classes carry a mandatory
  2245 "class" prefix.  INCOMPATIBILITY.
  2246 
  2247 * Vacuous class specifications observe default sort.  INCOMPATIBILITY.
  2248 
  2249 * Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use
  2250 'class' instead.
  2251 
  2252 * Command 'code_reflect' allows to incorporate generated ML code into
  2253 runtime environment; replaces immature code_datatype antiquotation.
  2254 INCOMPATIBILITY.
  2255 
  2256 * Code generator: simple concept for abstract datatypes obeying
  2257 invariants.
  2258 
  2259 * Code generator: details of internal data cache have no impact on the
  2260 user space functionality any longer.
  2261 
  2262 * Methods "unfold_locales" and "intro_locales" ignore non-locale
  2263 subgoals.  This is more appropriate for interpretations with 'where'.
  2264 INCOMPATIBILITY.
  2265 
  2266 * Command 'example_proof' opens an empty proof body.  This allows to
  2267 experiment with Isar, without producing any persistent result.
  2268 
  2269 * Commands 'type_notation' and 'no_type_notation' declare type syntax
  2270 within a local theory context, with explicit checking of the
  2271 constructors involved (in contrast to the raw 'syntax' versions).
  2272 
  2273 * Commands 'types' and 'typedecl' now work within a local theory
  2274 context -- without introducing dependencies on parameters or
  2275 assumptions, which is not possible in Isabelle/Pure.
  2276 
  2277 * Command 'defaultsort' has been renamed to 'default_sort', it works
  2278 within a local theory context.  Minor INCOMPATIBILITY.
  2279 
  2280 
  2281 *** HOL ***
  2282 
  2283 * Command 'typedef' now works within a local theory context -- without
  2284 introducing dependencies on parameters or assumptions, which is not
  2285 possible in Isabelle/Pure/HOL.  Note that the logical environment may
  2286 contain multiple interpretations of local typedefs (with different
  2287 non-emptiness proofs), even in a global theory context.
  2288 
  2289 * New package for quotient types.  Commands 'quotient_type' and
  2290 'quotient_definition' may be used for defining types and constants by
  2291 quotient constructions.  An example is the type of integers created by
  2292 quotienting pairs of natural numbers:
  2293 
  2294   fun
  2295     intrel :: "(nat * nat) => (nat * nat) => bool"
  2296   where
  2297     "intrel (x, y) (u, v) = (x + v = u + y)"
  2298 
  2299   quotient_type int = "nat * nat" / intrel
  2300     by (auto simp add: equivp_def expand_fun_eq)
  2301 
  2302   quotient_definition
  2303     "0::int" is "(0::nat, 0::nat)"
  2304 
  2305 The method "lifting" can be used to lift of theorems from the
  2306 underlying "raw" type to the quotient type.  The example
  2307 src/HOL/Quotient_Examples/FSet.thy includes such a quotient
  2308 construction and provides a reasoning infrastructure for finite sets.
  2309 
  2310 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
  2311 clash with new theory Quotient in Main HOL.
  2312 
  2313 * Moved the SMT binding into the main HOL session, eliminating
  2314 separate HOL-SMT session.
  2315 
  2316 * List membership infix mem operation is only an input abbreviation.
  2317 INCOMPATIBILITY.
  2318 
  2319 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy
  2320 for future developements; former Library/Word.thy is still present in
  2321 the AFP entry RSAPPS.
  2322 
  2323 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
  2324 longer shadowed.  INCOMPATIBILITY.
  2325 
  2326 * Dropped theorem duplicate comp_arith; use semiring_norm instead.
  2327 INCOMPATIBILITY.
  2328 
  2329 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
  2330 INCOMPATIBILITY.
  2331 
  2332 * Dropped normalizing_semiring etc; use the facts in semiring classes
  2333 instead.  INCOMPATIBILITY.
  2334 
  2335 * Dropped several real-specific versions of lemmas about floor and
  2336 ceiling; use the generic lemmas from theory "Archimedean_Field"
  2337 instead.  INCOMPATIBILITY.
  2338 
  2339   floor_number_of_eq         ~> floor_number_of
  2340   le_floor_eq_number_of      ~> number_of_le_floor
  2341   le_floor_eq_zero           ~> zero_le_floor
  2342   le_floor_eq_one            ~> one_le_floor
  2343   floor_less_eq_number_of    ~> floor_less_number_of
  2344   floor_less_eq_zero         ~> floor_less_zero
  2345   floor_less_eq_one          ~> floor_less_one
  2346   less_floor_eq_number_of    ~> number_of_less_floor
  2347   less_floor_eq_zero         ~> zero_less_floor
  2348   less_floor_eq_one          ~> one_less_floor
  2349   floor_le_eq_number_of      ~> floor_le_number_of
  2350   floor_le_eq_zero           ~> floor_le_zero
  2351   floor_le_eq_one            ~> floor_le_one
  2352   floor_subtract_number_of   ~> floor_diff_number_of
  2353   floor_subtract_one         ~> floor_diff_one
  2354   ceiling_number_of_eq       ~> ceiling_number_of
  2355   ceiling_le_eq_number_of    ~> ceiling_le_number_of
  2356   ceiling_le_zero_eq         ~> ceiling_le_zero
  2357   ceiling_le_eq_one          ~> ceiling_le_one
  2358   less_ceiling_eq_number_of  ~> number_of_less_ceiling
  2359   less_ceiling_eq_zero       ~> zero_less_ceiling
  2360   less_ceiling_eq_one        ~> one_less_ceiling
  2361   ceiling_less_eq_number_of  ~> ceiling_less_number_of
  2362   ceiling_less_eq_zero       ~> ceiling_less_zero
  2363   ceiling_less_eq_one        ~> ceiling_less_one
  2364   le_ceiling_eq_number_of    ~> number_of_le_ceiling
  2365   le_ceiling_eq_zero         ~> zero_le_ceiling
  2366   le_ceiling_eq_one          ~> one_le_ceiling
  2367   ceiling_subtract_number_of ~> ceiling_diff_number_of
  2368   ceiling_subtract_one       ~> ceiling_diff_one
  2369 
  2370 * Theory "Finite_Set": various folding_XXX locales facilitate the
  2371 application of the various fold combinators on finite sets.
  2372 
  2373 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
  2374 provides abstract red-black tree type which is backed by "RBT_Impl" as
  2375 implementation.  INCOMPATIBILTY.
  2376 
  2377 * Theory Library/Coinductive_List has been removed -- superseded by
  2378 AFP/thys/Coinductive.
  2379 
  2380 * Theory PReal, including the type "preal" and related operations, has
  2381 been removed.  INCOMPATIBILITY.
  2382 
  2383 * Real: new development using Cauchy Sequences.
  2384 
  2385 * Split off theory "Big_Operators" containing setsum, setprod,
  2386 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
  2387 
  2388 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
  2389 "Int" etc.  INCOMPATIBILITY.
  2390 
  2391 * Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.
  2392 
  2393 * New set of rules "ac_simps" provides combined assoc / commute
  2394 rewrites for all interpretations of the appropriate generic locales.
  2395 
  2396 * Renamed theory "OrderedGroup" to "Groups" and split theory
  2397 "Ring_and_Field" into theories "Rings" and "Fields"; for more
  2398 appropriate and more consistent names suitable for name prefixes
  2399 within the HOL theories.  INCOMPATIBILITY.
  2400 
  2401 * Some generic constants have been put to appropriate theories:
  2402   - less_eq, less: Orderings
  2403   - zero, one, plus, minus, uminus, times, abs, sgn: Groups
  2404   - inverse, divide: Rings
  2405 INCOMPATIBILITY.
  2406 
  2407 * More consistent naming of type classes involving orderings (and
  2408 lattices):
  2409 
  2410     lower_semilattice                   ~> semilattice_inf
  2411     upper_semilattice                   ~> semilattice_sup
  2412 
  2413     dense_linear_order                  ~> dense_linorder
  2414 
  2415     pordered_ab_group_add               ~> ordered_ab_group_add
  2416     pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
  2417     pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
  2418     pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
  2419     pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
  2420     pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
  2421     pordered_cancel_semiring            ~> ordered_cancel_semiring
  2422     pordered_comm_monoid_add            ~> ordered_comm_monoid_add
  2423     pordered_comm_ring                  ~> ordered_comm_ring
  2424     pordered_comm_semiring              ~> ordered_comm_semiring
  2425     pordered_ring                       ~> ordered_ring
  2426     pordered_ring_abs                   ~> ordered_ring_abs
  2427     pordered_semiring                   ~> ordered_semiring
  2428 
  2429     ordered_ab_group_add                ~> linordered_ab_group_add
  2430     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
  2431     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
  2432     ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
  2433     ordered_field                       ~> linordered_field
  2434     ordered_field_no_lb                 ~> linordered_field_no_lb
  2435     ordered_field_no_ub                 ~> linordered_field_no_ub
  2436     ordered_field_dense_linear_order    ~> dense_linordered_field
  2437     ordered_idom                        ~> linordered_idom
  2438     ordered_ring                        ~> linordered_ring
  2439     ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
  2440     ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
  2441     ordered_ring_strict                 ~> linordered_ring_strict
  2442     ordered_semidom                     ~> linordered_semidom
  2443     ordered_semiring                    ~> linordered_semiring
  2444     ordered_semiring_1                  ~> linordered_semiring_1
  2445     ordered_semiring_1_strict           ~> linordered_semiring_1_strict
  2446     ordered_semiring_strict             ~> linordered_semiring_strict
  2447 
  2448   The following slightly odd type classes have been moved to a
  2449   separate theory Library/Lattice_Algebras:
  2450 
  2451     lordered_ab_group_add               ~> lattice_ab_group_add
  2452     lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
  2453     lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
  2454     lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
  2455     lordered_ring                       ~> lattice_ring
  2456 
  2457 INCOMPATIBILITY.
  2458 
  2459 * Refined field classes:
  2460   - classes division_ring_inverse_zero, field_inverse_zero,
  2461     linordered_field_inverse_zero include rule inverse 0 = 0 --
  2462     subsumes former division_by_zero class;
  2463   - numerous lemmas have been ported from field to division_ring.
  2464 INCOMPATIBILITY.
  2465 
  2466 * Refined algebra theorem collections:
  2467   - dropped theorem group group_simps, use algebra_simps instead;
  2468   - dropped theorem group ring_simps, use field_simps instead;
  2469   - proper theorem collection field_simps subsumes former theorem
  2470     groups field_eq_simps and field_simps;
  2471   - dropped lemma eq_minus_self_iff which is a duplicate for
  2472     equal_neg_zero.
  2473 INCOMPATIBILITY.
  2474 
  2475 * Theory Finite_Set and List: some lemmas have been generalized from
  2476 sets to lattices:
  2477 
  2478   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
  2479   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
  2480   inter_Inter_fold_inter        ~> inf_Inf_fold_inf
  2481   union_Union_fold_union        ~> sup_Sup_fold_sup
  2482   Inter_fold_inter              ~> Inf_fold_inf
  2483   Union_fold_union              ~> Sup_fold_sup
  2484   inter_INTER_fold_inter        ~> inf_INFI_fold_inf
  2485   union_UNION_fold_union        ~> sup_SUPR_fold_sup
  2486   INTER_fold_inter              ~> INFI_fold_inf
  2487   UNION_fold_union              ~> SUPR_fold_sup
  2488 
  2489 * Theory "Complete_Lattice": lemmas top_def and bot_def have been
  2490 replaced by the more convenient lemmas Inf_empty and Sup_empty.
  2491 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
  2492 by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
  2493 former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
  2494 subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
  2495 
  2496 * Reorganized theory Multiset: swapped notation of pointwise and
  2497 multiset order:
  2498 
  2499   - pointwise ordering is instance of class order with standard syntax
  2500     <= and <;
  2501   - multiset ordering has syntax <=# and <#; partial order properties
  2502     are provided by means of interpretation with prefix
  2503     multiset_order;
  2504   - less duplication, less historical organization of sections,
  2505     conversion from associations lists to multisets, rudimentary code
  2506     generation;
  2507   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
  2508     if needed.
  2509 
  2510 Renamed:
  2511 
  2512   multiset_eq_conv_count_eq  ~>  multiset_ext_iff
  2513   multi_count_ext  ~>  multiset_ext
  2514   diff_union_inverse2  ~>  diff_union_cancelR
  2515 
  2516 INCOMPATIBILITY.
  2517 
  2518 * Theory Permutation: replaced local "remove" by List.remove1.
  2519 
  2520 * Code generation: ML and OCaml code is decorated with signatures.
  2521 
  2522 * Theory List: added transpose.
  2523 
  2524 * Library/Nat_Bijection.thy is a collection of bijective functions
  2525 between nat and other types, which supersedes the older libraries
  2526 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
  2527 
  2528   Constants:
  2529   Nat_Int_Bij.nat2_to_nat         ~> prod_encode
  2530   Nat_Int_Bij.nat_to_nat2         ~> prod_decode
  2531   Nat_Int_Bij.int_to_nat_bij      ~> int_encode
  2532   Nat_Int_Bij.nat_to_int_bij      ~> int_decode
  2533   Countable.pair_encode           ~> prod_encode
  2534   NatIso.prod2nat                 ~> prod_encode
  2535   NatIso.nat2prod                 ~> prod_decode
  2536   NatIso.sum2nat                  ~> sum_encode
  2537   NatIso.nat2sum                  ~> sum_decode
  2538   NatIso.list2nat                 ~> list_encode
  2539   NatIso.nat2list                 ~> list_decode
  2540   NatIso.set2nat                  ~> set_encode
  2541   NatIso.nat2set                  ~> set_decode
  2542 
  2543   Lemmas:
  2544   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
  2545   Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
  2546   Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
  2547   Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
  2548   Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
  2549   Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
  2550   Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
  2551   Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
  2552   Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
  2553   Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
  2554   Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
  2555   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
  2556   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
  2557 
  2558 * Sledgehammer:
  2559   - Renamed ATP commands:
  2560     atp_info     ~> sledgehammer running_atps
  2561     atp_kill     ~> sledgehammer kill_atps
  2562     atp_messages ~> sledgehammer messages
  2563     atp_minimize ~> sledgehammer minimize
  2564     print_atps   ~> sledgehammer available_atps
  2565     INCOMPATIBILITY.
  2566   - Added user's manual ("isabelle doc sledgehammer").
  2567   - Added option syntax and "sledgehammer_params" to customize
  2568     Sledgehammer's behavior.  See the manual for details.
  2569   - Modified the Isar proof reconstruction code so that it produces
  2570     direct proofs rather than proofs by contradiction.  (This feature
  2571     is still experimental.)
  2572   - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
  2573     full-typed mode.
  2574   - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
  2575 
  2576 * Nitpick:
  2577   - Added and implemented "binary_ints" and "bits" options.
  2578   - Added "std" option and implemented support for nonstandard models.
  2579   - Added and implemented "finitize" option to improve the precision
  2580     of infinite datatypes based on a monotonicity analysis.
  2581   - Added support for quotient types.
  2582   - Added support for "specification" and "ax_specification"
  2583     constructs.
  2584   - Added support for local definitions (for "function" and
  2585     "termination" proofs).
  2586   - Added support for term postprocessors.
  2587   - Optimized "Multiset.multiset" and "FinFun.finfun".
  2588   - Improved efficiency of "destroy_constrs" optimization.
  2589   - Fixed soundness bugs related to "destroy_constrs" optimization and
  2590     record getters.
  2591   - Fixed soundness bug related to higher-order constructors.
  2592   - Fixed soundness bug when "full_descrs" is enabled.
  2593   - Improved precision of set constructs.
  2594   - Added "atoms" option.
  2595   - Added cache to speed up repeated Kodkod invocations on the same
  2596     problems.
  2597   - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
  2598     "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
  2599     "SAT4J_Light".  INCOMPATIBILITY.
  2600   - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
  2601     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
  2602   - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
  2603 
  2604 * Method "induct" now takes instantiations of the form t, where t is not
  2605   a variable, as a shorthand for "x == t", where x is a fresh variable.
  2606   If this is not intended, t has to be enclosed in parentheses.
  2607   By default, the equalities generated by definitional instantiations
  2608   are pre-simplified, which may cause parameters of inductive cases
  2609   to disappear, or may even delete some of the inductive cases.
  2610   Use "induct (no_simp)" instead of "induct" to restore the old
  2611   behaviour. The (no_simp) option is also understood by the "cases"
  2612   and "nominal_induct" methods, which now perform pre-simplification, too.
  2613   INCOMPATIBILITY.
  2614 
  2615 
  2616 *** HOLCF ***
  2617 
  2618 * Variable names in lemmas generated by the domain package have
  2619 changed; the naming scheme is now consistent with the HOL datatype
  2620 package.  Some proof scripts may be affected, INCOMPATIBILITY.
  2621 
  2622 * The domain package no longer defines the function "foo_copy" for
  2623 recursive domain "foo".  The reach lemma is now stated directly in
  2624 terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
  2625 be reformulated in terms of "foo_take", INCOMPATIBILITY.
  2626 
  2627 * Most definedness lemmas generated by the domain package (previously
  2628 of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
  2629 like "foo$x = UU <-> x = UU", which works better as a simp rule.
  2630 Proofs that used definedness lemmas as intro rules may break,
  2631 potential INCOMPATIBILITY.
  2632 
  2633 * Induction and casedist rules generated by the domain package now
  2634 declare proper case_names (one called "bottom", and one named for each
  2635 constructor).  INCOMPATIBILITY.
  2636 
  2637 * For mutually-recursive domains, separate "reach" and "take_lemma"
  2638 rules are generated for each domain, INCOMPATIBILITY.
  2639 
  2640   foo_bar.reach       ~> foo.reach  bar.reach
  2641   foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
  2642 
  2643 * Some lemmas generated by the domain package have been renamed for
  2644 consistency with the datatype package, INCOMPATIBILITY.
  2645 
  2646   foo.ind        ~> foo.induct
  2647   foo.finite_ind ~> foo.finite_induct
  2648   foo.coind      ~> foo.coinduct
  2649   foo.casedist   ~> foo.exhaust
  2650   foo.exhaust    ~> foo.nchotomy
  2651 
  2652 * For consistency with other definition packages, the fixrec package
  2653 now generates qualified theorem names, INCOMPATIBILITY.
  2654 
  2655   foo_simps  ~> foo.simps
  2656   foo_unfold ~> foo.unfold
  2657   foo_induct ~> foo.induct
  2658 
  2659 * The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
  2660 method and internal fixrec proofs now use the default simpset instead.
  2661 INCOMPATIBILITY.
  2662 
  2663 * The "contlub" predicate has been removed.  Proof scripts should use
  2664 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
  2665 
  2666 * The "admw" predicate has been removed, INCOMPATIBILITY.
  2667 
  2668 * The constants cpair, cfst, and csnd have been removed in favor of
  2669 Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
  2670 
  2671 
  2672 *** ML ***
  2673 
  2674 * Antiquotations for basic formal entities:
  2675 
  2676     @{class NAME}         -- type class
  2677     @{class_syntax NAME}  -- syntax representation of the above
  2678 
  2679     @{type_name NAME}     -- logical type
  2680     @{type_abbrev NAME}   -- type abbreviation
  2681     @{nonterminal NAME}   -- type of concrete syntactic category
  2682     @{type_syntax NAME}   -- syntax representation of any of the above
  2683 
  2684     @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
  2685     @{const_abbrev NAME}  -- abbreviated constant
  2686     @{const_syntax NAME}  -- syntax representation of any of the above
  2687 
  2688 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
  2689 syntax constant (cf. 'syntax' command).
  2690 
  2691 * Antiquotation @{make_string} inlines a function to print arbitrary
  2692 values similar to the ML toplevel.  The result is compiler dependent
  2693 and may fall back on "?" in certain situations.
  2694 
  2695 * Diagnostic commands 'ML_val' and 'ML_command' may refer to
  2696 antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
  2697 Isar.state() and Isar.goal(), which belong to the old TTY loop and do
  2698 not work with the asynchronous Isar document model.
  2699 
  2700 * Configuration options now admit dynamic default values, depending on
  2701 the context or even global references.
  2702 
  2703 * SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
  2704 uses an efficient external library if available (for Poly/ML).
  2705 
  2706 * Renamed some important ML structures, while keeping the old names
  2707 for some time as aliases within the structure Legacy:
  2708 
  2709   OuterKeyword  ~>  Keyword
  2710   OuterLex      ~>  Token
  2711   OuterParse    ~>  Parse
  2712   OuterSyntax   ~>  Outer_Syntax
  2713   PrintMode     ~>  Print_Mode
  2714   SpecParse     ~>  Parse_Spec
  2715   ThyInfo       ~>  Thy_Info
  2716   ThyLoad       ~>  Thy_Load
  2717   ThyOutput     ~>  Thy_Output
  2718   TypeInfer     ~>  Type_Infer
  2719 
  2720 Note that "open Legacy" simplifies porting of sources, but forgetting
  2721 to remove it again will complicate porting again in the future.
  2722 
  2723 * Most operations that refer to a global context are named
  2724 accordingly, e.g. Simplifier.global_context or
  2725 ProofContext.init_global.  There are some situations where a global
  2726 context actually works, but under normal circumstances one needs to
  2727 pass the proper local context through the code!
  2728 
  2729 * Discontinued old TheoryDataFun with its copy/init operation -- data
  2730 needs to be pure.  Functor Theory_Data_PP retains the traditional
  2731 Pretty.pp argument to merge, which is absent in the standard
  2732 Theory_Data version.
  2733 
  2734 * Sorts.certify_sort and derived "cert" operations for types and terms
  2735 no longer minimize sorts.  Thus certification at the boundary of the
  2736 inference kernel becomes invariant under addition of class relations,
  2737 which is an important monotonicity principle.  Sorts are now minimized
  2738 in the syntax layer only, at the boundary between the end-user and the
  2739 system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
  2740 explicitly in rare situations.
  2741 
  2742 * Renamed old-style Drule.standard to Drule.export_without_context, to
  2743 emphasize that this is in no way a standard operation.
  2744 INCOMPATIBILITY.
  2745 
  2746 * Subgoal.FOCUS (and variants): resulting goal state is normalized as
  2747 usual for resolution.  Rare INCOMPATIBILITY.
  2748 
  2749 * Renamed varify/unvarify operations to varify_global/unvarify_global
  2750 to emphasize that these only work in a global situation (which is
  2751 quite rare).
  2752 
  2753 * Curried take and drop in library.ML; negative length is interpreted
  2754 as infinity (as in chop).  Subtle INCOMPATIBILITY.
  2755 
  2756 * Proof terms: type substitutions on proof constants now use canonical
  2757 order of type variables.  INCOMPATIBILITY for tools working with proof
  2758 terms.
  2759 
  2760 * Raw axioms/defs may no longer carry sort constraints, and raw defs
  2761 may no longer carry premises.  User-level specifications are
  2762 transformed accordingly by Thm.add_axiom/add_def.
  2763 
  2764 
  2765 *** System ***
  2766 
  2767 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
  2768 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
  2769 proof terms are enabled unconditionally in the new HOL-Proofs image.
  2770 
  2771 * Discontinued old ISABELLE and ISATOOL environment settings (legacy
  2772 feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
  2773 respectively.
  2774 
  2775 * Old lib/scripts/polyml-platform is superseded by the
  2776 ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
  2777 variant, even on a 64 bit machine.  The following example setting
  2778 prefers 64 bit if available:
  2779 
  2780   ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
  2781 
  2782 * The preliminary Isabelle/jEdit application demonstrates the emerging
  2783 Isabelle/Scala layer for advanced prover interaction and integration.
  2784 See src/Tools/jEdit or "isabelle jedit" provided by the properly built
  2785 component.
  2786 
  2787 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
  2788 and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
  2789 similar to the default assignment of the document preparation system
  2790 (cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
  2791 provides some operations for direct access to the font without asking
  2792 the user for manual installation.
  2793 
  2794 
  2795 
  2796 New in Isabelle2009-1 (December 2009)
  2797 -------------------------------------
  2798 
  2799 *** General ***
  2800 
  2801 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only
  2802 one backslash should be used, even in ML sources.
  2803 
  2804 
  2805 *** Pure ***
  2806 
  2807 * Locale interpretation propagates mixins along the locale hierarchy.
  2808 The currently only available mixins are the equations used to map
  2809 local definitions to terms of the target domain of an interpretation.
  2810 
  2811 * Reactivated diagnostic command 'print_interps'.  Use "print_interps
  2812 loc" to print all interpretations of locale "loc" in the theory.
  2813 Interpretations in proofs are not shown.
  2814 
  2815 * Thoroughly revised locales tutorial.  New section on conditional
  2816 interpretation.
  2817 
  2818 * On instantiation of classes, remaining undefined class parameters
  2819 are formally declared.  INCOMPATIBILITY.
  2820 
  2821 
  2822 *** Document preparation ***
  2823 
  2824 * New generalized style concept for printing terms: @{foo (style) ...}
  2825 instead of @{foo_style style ...}  (old form is still retained for
  2826 backward compatibility).  Styles can be also applied for
  2827 antiquotations prop, term_type and typeof.
  2828 
  2829 
  2830 *** HOL ***
  2831 
  2832 * New proof method "smt" for a combination of first-order logic with
  2833 equality, linear and nonlinear (natural/integer/real) arithmetic, and
  2834 fixed-size bitvectors; there is also basic support for higher-order
  2835 features (esp. lambda abstractions).  It is an incomplete decision
  2836 procedure based on external SMT solvers using the oracle mechanism;
  2837 for the SMT solver Z3, this method is proof-producing.  Certificates
  2838 are provided to avoid calling the external solvers solely for
  2839 re-checking proofs.  Due to a remote SMT service there is no need for
  2840 installing SMT solvers locally.  See src/HOL/SMT.
  2841 
  2842 * New commands to load and prove verification conditions generated by
  2843 the Boogie program verifier or derived systems (e.g. the Verifying C
  2844 Compiler (VCC) or Spec#).  See src/HOL/Boogie.
  2845 
  2846 * New counterexample generator tool 'nitpick' based on the Kodkod
  2847 relational model finder.  See src/HOL/Tools/Nitpick and
  2848 src/HOL/Nitpick_Examples.
  2849 
  2850 * New commands 'code_pred' and 'values' to invoke the predicate
  2851 compiler and to enumerate values of inductive predicates.
  2852 
  2853 * A tabled implementation of the reflexive transitive closure.
  2854 
  2855 * New implementation of quickcheck uses generic code generator;
  2856 default generators are provided for all suitable HOL types, records
  2857 and datatypes.  Old quickcheck can be re-activated importing theory
  2858 Library/SML_Quickcheck.
  2859 
  2860 * New testing tool Mirabelle for automated proof tools.  Applies
  2861 several tools and tactics like sledgehammer, metis, or quickcheck, to
  2862 every proof step in a theory.  To be used in batch mode via the
  2863 "mirabelle" utility.
  2864 
  2865 * New proof method "sos" (sum of squares) for nonlinear real
  2866 arithmetic (originally due to John Harison). It requires theory
  2867 Library/Sum_Of_Squares.  It is not a complete decision procedure but
  2868 works well in practice on quantifier-free real arithmetic with +, -,
  2869 *, ^, =, <= and <, i.e. boolean combinations of equalities and
  2870 inequalities between polynomials.  It makes use of external
  2871 semidefinite programming solvers.  Method "sos" generates a
  2872 certificate that can be pasted into the proof thus avoiding the need
  2873 to call an external tool every time the proof is checked.  See
  2874 src/HOL/Library/Sum_Of_Squares.
  2875 
  2876 * New method "linarith" invokes existing linear arithmetic decision
  2877 procedure only.
  2878 
  2879 * New command 'atp_minimal' reduces result produced by Sledgehammer.
  2880 
  2881 * New Sledgehammer option "Full Types" in Proof General settings menu.
  2882 Causes full type information to be output to the ATPs.  This slows
  2883 ATPs down considerably but eliminates a source of unsound "proofs"
  2884 that fail later.
  2885 
  2886 * New method "metisFT": A version of metis that uses full type
  2887 information in order to avoid failures of proof reconstruction.
  2888 
  2889 * New evaluator "approximate" approximates an real valued term using
  2890 the same method as the approximation method.
  2891 
  2892 * Method "approximate" now supports arithmetic expressions as
  2893 boundaries of intervals and implements interval splitting and Taylor
  2894 series expansion.
  2895 
  2896 * ML antiquotation @{code_datatype} inserts definition of a datatype
  2897 generated by the code generator; e.g. see src/HOL/Predicate.thy.
  2898 
  2899 * New theory SupInf of the supremum and infimum operators for sets of
  2900 reals.
  2901 
  2902 * New theory Probability, which contains a development of measure
  2903 theory, eventually leading to Lebesgue integration and probability.
  2904 
  2905 * Extended Multivariate Analysis to include derivation and Brouwer's
  2906 fixpoint theorem.
  2907 
  2908 * Reorganization of number theory, INCOMPATIBILITY:
  2909   - new number theory development for nat and int, in theories Divides
  2910     and GCD as well as in new session Number_Theory
  2911   - some constants and facts now suffixed with _nat and _int
  2912     accordingly
  2913   - former session NumberTheory now named Old_Number_Theory, including
  2914     theories Legacy_GCD and Primes (prefer Number_Theory if possible)
  2915   - moved theory Pocklington from src/HOL/Library to
  2916     src/HOL/Old_Number_Theory
  2917 
  2918 * Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
  2919 lcm of finite and infinite sets. It is shown that they form a complete
  2920 lattice.
  2921 
  2922 * Class semiring_div requires superclass no_zero_divisors and proof of
  2923 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
  2924 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
  2925 generalized to class semiring_div, subsuming former theorems
  2926 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
  2927 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
  2928 INCOMPATIBILITY.
  2929 
  2930 * Refinements to lattice classes and sets:
  2931   - less default intro/elim rules in locale variant, more default
  2932     intro/elim rules in class variant: more uniformity
  2933   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
  2934     le_inf_iff
  2935   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
  2936     sup_aci)
  2937   - renamed ACI to inf_sup_aci
  2938   - new class "boolean_algebra"
  2939   - class "complete_lattice" moved to separate theory
  2940     "Complete_Lattice"; corresponding constants (and abbreviations)
  2941     renamed and with authentic syntax:
  2942     Set.Inf ~>    Complete_Lattice.Inf
  2943     Set.Sup ~>    Complete_Lattice.Sup
  2944     Set.INFI ~>   Complete_Lattice.INFI
  2945     Set.SUPR ~>   Complete_Lattice.SUPR
  2946     Set.Inter ~>  Complete_Lattice.Inter
  2947     Set.Union ~>  Complete_Lattice.Union
  2948     Set.INTER ~>  Complete_Lattice.INTER
  2949     Set.UNION ~>  Complete_Lattice.UNION
  2950   - authentic syntax for
  2951     Set.Pow
  2952     Set.image
  2953   - mere abbreviations:
  2954     Set.empty               (for bot)
  2955     Set.UNIV                (for top)
  2956     Set.inter               (for inf, formerly Set.Int)
  2957     Set.union               (for sup, formerly Set.Un)
  2958     Complete_Lattice.Inter  (for Inf)
  2959     Complete_Lattice.Union  (for Sup)
  2960     Complete_Lattice.INTER  (for INFI)
  2961     Complete_Lattice.UNION  (for SUPR)
  2962   - object-logic definitions as far as appropriate
  2963 
  2964 INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
  2965 Un_subset_iff are explicitly deleted as default simp rules; then also
  2966 their lattice counterparts le_inf_iff and le_sup_iff have to be
  2967 deleted to achieve the desired effect.
  2968 
  2969 * Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
  2970 rules by default any longer; the same applies to min_max.inf_absorb1
  2971 etc.  INCOMPATIBILITY.
  2972 
  2973 * Rules sup_Int_eq and sup_Un_eq are no longer declared as
  2974 pred_set_conv by default.  INCOMPATIBILITY.
  2975 
  2976 * Power operations on relations and functions are now one dedicated
  2977 constant "compow" with infix syntax "^^".  Power operation on
  2978 multiplicative monoids retains syntax "^" and is now defined generic
  2979 in class power.  INCOMPATIBILITY.
  2980 
  2981 * Relation composition "R O S" now has a more standard argument order:
  2982 "R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,
  2983 rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
  2984 break, since the O_assoc rule was not rewritten like this.  Fix using
  2985 O_assoc[symmetric].  The same applies to the curried version "R OO S".
  2986 
  2987 * Function "Inv" is renamed to "inv_into" and function "inv" is now an
  2988 abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
  2989 INCOMPATIBILITY.
  2990 
  2991 * Most rules produced by inductive and datatype package have mandatory
  2992 prefixes.  INCOMPATIBILITY.
  2993 
  2994 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by
  2995 the attribute of the same name.  Each of the theorems in the list
  2996 DERIV_intros assumes composition with an additional function and
  2997 matches a variable to the derivative, which has to be solved by the
  2998 Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
  2999 of most elementary terms.  Former Maclauren.DERIV_tac and
  3000 Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
  3001 INCOMPATIBILITY.
  3002 
  3003 * Code generator attributes follow the usual underscore convention:
  3004     code_unfold     replaces    code unfold
  3005     code_post       replaces    code post
  3006     etc.
  3007   INCOMPATIBILITY.
  3008 
  3009 * Renamed methods:
  3010     sizechange -> size_change
  3011     induct_scheme -> induction_schema
  3012   INCOMPATIBILITY.
  3013 
  3014 * Discontinued abbreviation "arbitrary" of constant "undefined".
  3015 INCOMPATIBILITY, use "undefined" directly.
  3016 
  3017 * Renamed theorems:
  3018     Suc_eq_add_numeral_1 -> Suc_eq_plus1
  3019     Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
  3020     Suc_plus1 -> Suc_eq_plus1
  3021     *anti_sym -> *antisym*
  3022     vector_less_eq_def -> vector_le_def
  3023   INCOMPATIBILITY.
  3024 
  3025 * Added theorem List.map_map as [simp].  Removed List.map_compose.
  3026 INCOMPATIBILITY.
  3027 
  3028 * Removed predicate "M hassize n" (<--> card M = n & finite M).
  3029 INCOMPATIBILITY.
  3030 
  3031 
  3032 *** HOLCF ***
  3033 
  3034 * Theory Representable defines a class "rep" of domains that are
  3035 representable (via an ep-pair) in the universal domain type "udom".
  3036 Instances are provided for all type constructors defined in HOLCF.
  3037 
  3038 * The 'new_domain' command is a purely definitional version of the
  3039 domain package, for representable domains.  Syntax is identical to the
  3040 old domain package.  The 'new_domain' package also supports indirect
  3041 recursion using previously-defined type constructors.  See
  3042 src/HOLCF/ex/New_Domain.thy for examples.
  3043 
  3044 * Method "fixrec_simp" unfolds one step of a fixrec-defined constant
  3045 on the left-hand side of an equation, and then performs
  3046 simplification.  Rewriting is done using rules declared with the
  3047 "fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
  3048 replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
  3049 
  3050 * The pattern-match compiler in 'fixrec' can now handle constructors
  3051 with HOL function types.  Pattern-match combinators for the Pair
  3052 constructor are pre-configured.
  3053 
  3054 * The 'fixrec' package now produces better fixed-point induction rules
  3055 for mutually-recursive definitions:  Induction rules have conclusions
  3056 of the form "P foo bar" instead of "P <foo, bar>".
  3057 
  3058 * The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
  3059 been renamed to "below".  The name "below" now replaces "less" in many
  3060 theorem names.  (Legacy theorem names using "less" are still supported
  3061 as well.)
  3062 
  3063 * The 'fixrec' package now supports "bottom patterns".  Bottom
  3064 patterns can be used to generate strictness rules, or to make
  3065 functions more strict (much like the bang-patterns supported by the
  3066 Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
  3067 examples.
  3068 
  3069 
  3070 *** ML ***
  3071 
  3072 * Support for Poly/ML 5.3.0, with improved reporting of compiler
  3073 errors and run-time exceptions, including detailed source positions.
  3074 
  3075 * Structure Name_Space (formerly NameSpace) now manages uniquely
  3076 identified entries, with some additional information such as source
  3077 position, logical grouping etc.
  3078 
  3079 * Theory and context data is now introduced by the simplified and
  3080 modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
  3081 to be pure, but the old TheoryDataFun for mutable data (with explicit
  3082 copy operation) is still available for some time.
  3083 
  3084 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
  3085 provides a high-level programming interface to synchronized state
  3086 variables with atomic update.  This works via pure function
  3087 application within a critical section -- its runtime should be as
  3088 short as possible; beware of deadlocks if critical code is nested,
  3089 either directly or indirectly via other synchronized variables!
  3090 
  3091 * Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
  3092 wraps raw ML references, explicitly indicating their non-thread-safe
  3093 behaviour.  The Isar toplevel keeps this structure open, to
  3094 accommodate Proof General as well as quick and dirty interactive
  3095 experiments with references.
  3096 
  3097 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
  3098 parallel tactical reasoning.
  3099 
  3100 * Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
  3101 are similar to SUBPROOF, but are slightly more flexible: only the
  3102 specified parts of the subgoal are imported into the context, and the
  3103 body tactic may introduce new subgoals and schematic variables.
  3104 
  3105 * Old tactical METAHYPS, which does not observe the proof context, has
  3106 been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
  3107 or Subgoal.FOCUS etc.
  3108 
  3109 * Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
  3110 functors have their own ML name space there is no point to mark them
  3111 separately.)  Minor INCOMPATIBILITY.
  3112 
  3113 * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
  3114 
  3115 * Renamed several structures FooBar to Foo_Bar.  Occasional,
  3116 INCOMPATIBILITY.
  3117 
  3118 * Operations of structure Skip_Proof no longer require quick_and_dirty
  3119 mode, which avoids critical setmp.
  3120 
  3121 * Eliminated old Attrib.add_attributes, Method.add_methods and related
  3122 combinators for "args".  INCOMPATIBILITY, need to use simplified
  3123 Attrib/Method.setup introduced in Isabelle2009.
  3124 
  3125 * Proper context for simpset_of, claset_of, clasimpset_of.  May fall
  3126 back on global_simpset_of, global_claset_of, global_clasimpset_of as
  3127 last resort.  INCOMPATIBILITY.
  3128 
  3129 * Display.pretty_thm now requires a proper context (cf. former
  3130 ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
  3131 or even Display.pretty_thm_without_context as last resort.
  3132 INCOMPATIBILITY.
  3133 
  3134 * Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
  3135 Syntax.pretty_typ/term directly, preferably with proper context
  3136 instead of global theory.
  3137 
  3138 
  3139 *** System ***
  3140 
  3141 * Further fine tuning of parallel proof checking, scales up to 8 cores
  3142 (max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and
  3143 usedir option -q.
  3144 
  3145 * Support for additional "Isabelle components" via etc/components, see
  3146 also the system manual.
  3147 
  3148 * The isabelle makeall tool now operates on all components with
  3149 IsaMakefile, not just hardwired "logics".
  3150 
  3151 * Removed "compress" option from isabelle-process and isabelle usedir;
  3152 this is always enabled.
  3153 
  3154 * Discontinued support for Poly/ML 4.x versions.
  3155 
  3156 * Isabelle tool "wwwfind" provides web interface for 'find_theorems'
  3157 on a given logic image.  This requires the lighttpd webserver and is
  3158 currently supported on Linux only.
  3159 
  3160 
  3161 
  3162 New in Isabelle2009 (April 2009)
  3163 --------------------------------
  3164 
  3165 *** General ***
  3166 
  3167 * Simplified main Isabelle executables, with less surprises on
  3168 case-insensitive file-systems (such as Mac OS).
  3169 
  3170   - The main Isabelle tool wrapper is now called "isabelle" instead of
  3171     "isatool."
  3172 
  3173   - The former "isabelle" alias for "isabelle-process" has been
  3174     removed (should rarely occur to regular users).
  3175 
  3176   - The former "isabelle-interface" and its alias "Isabelle" have been
  3177     removed (interfaces are now regular Isabelle tools).
  3178 
  3179 Within scripts and make files, the Isabelle environment variables
  3180 ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
  3181 respectively.  (The latter are still available as legacy feature.)
  3182 
  3183 The old isabelle-interface wrapper could react in confusing ways if
  3184 the interface was uninstalled or changed otherwise.  Individual
  3185 interface tool configuration is now more explicit, see also the
  3186 Isabelle system manual.  In particular, Proof General is now available
  3187 via "isabelle emacs".
  3188 
  3189 INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to
  3190 purge installed copies of Isabelle executables and re-run "isabelle
  3191 install -p ...", or use symlinks.
  3192 
  3193 * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
  3194 old ~/isabelle, which was slightly non-standard and apt to cause
  3195 surprises on case-insensitive file-systems (such as Mac OS).
  3196 
  3197 INCOMPATIBILITY, need to move existing ~/isabelle/etc,
  3198 ~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special
  3199 care is required when using older releases of Isabelle.  Note that
  3200 ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
  3201 Isabelle distribution, in order to use the new ~/.isabelle uniformly.
  3202 
  3203 * Proofs of fully specified statements are run in parallel on
  3204 multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on
  3205 a regular 4-core machine, if the initial heap space is made reasonably
  3206 large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)
  3207 
  3208 * The main reference manuals ("isar-ref", "implementation", and
  3209 "system") have been updated and extended.  Formally checked references
  3210 as hyperlinks are now available uniformly.
  3211 
  3212 
  3213 *** Pure ***
  3214 
  3215 * Complete re-implementation of locales.  INCOMPATIBILITY in several
  3216 respects.  The most important changes are listed below.  See the
  3217 Tutorial on Locales ("locales" manual) for details.
  3218 
  3219 - In locale expressions, instantiation replaces renaming.  Parameters
  3220 must be declared in a for clause.  To aid compatibility with previous
  3221 parameter inheritance, in locale declarations, parameters that are not
  3222 'touched' (instantiation position "_" or omitted) are implicitly added
  3223 with their syntax at the beginning of the for clause.
  3224 
  3225 - Syntax from abbreviations and definitions in locales is available in
  3226 locale expressions and context elements.  The latter is particularly
  3227 useful in locale declarations.
  3228 
  3229 - More flexible mechanisms to qualify names generated by locale
  3230 expressions.  Qualifiers (prefixes) may be specified in locale
  3231 expressions, and can be marked as mandatory (syntax: "name!:") or
  3232 optional (syntax "name?:").  The default depends for plain "name:"
  3233 depends on the situation where a locale expression is used: in
  3234 commands 'locale' and 'sublocale' prefixes are optional, in
  3235 'interpretation' and 'interpret' prefixes are mandatory.  The old
  3236 implicit qualifiers derived from the parameter names of a locale are
  3237 no longer generated.
  3238 
  3239 - Command "sublocale l < e" replaces "interpretation l < e".  The
  3240 instantiation clause in "interpretation" and "interpret" (square
  3241 brackets) is no longer available.  Use locale expressions.
  3242 
  3243 - When converting proof scripts, mandatory qualifiers in
  3244 'interpretation' and 'interpret' should be retained by default, even
  3245 if this is an INCOMPATIBILITY compared to former behavior.  In the
  3246 worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
  3247 in locale expressions range over a single locale instance only.
  3248 
  3249 - Dropped locale element "includes".  This is a major INCOMPATIBILITY.
  3250 In existing theorem specifications replace the includes element by the
  3251 respective context elements of the included locale, omitting those
  3252 that are already present in the theorem specification.  Multiple
  3253 assume elements of a locale should be replaced by a single one
  3254 involving the locale predicate.  In the proof body, declarations (most
  3255 notably theorems) may be regained by interpreting the respective
  3256 locales in the proof context as required (command "interpret").
  3257 
  3258 If using "includes" in replacement of a target solely because the
  3259 parameter types in the theorem are not as general as in the target,
  3260 consider declaring a new locale with additional type constraints on
  3261 the parameters (context element "constrains").
  3262 
  3263 - Discontinued "locale (open)".  INCOMPATIBILITY.
  3264 
  3265 - Locale interpretation commands no longer attempt to simplify goal.
  3266 INCOMPATIBILITY: in rare situations the generated goal differs.  Use
  3267 methods intro_locales and unfold_locales to clarify.
  3268 
  3269 - Locale interpretation commands no longer accept interpretation
  3270 attributes.  INCOMPATIBILITY.
  3271 
  3272 * Class declaration: so-called "base sort" must not be given in import
  3273 list any longer, but is inferred from the specification.  Particularly
  3274 in HOL, write
  3275 
  3276     class foo = ...
  3277 
  3278 instead of
  3279 
  3280     class foo = type + ...
  3281 
  3282 * Class target: global versions of theorems stemming do not carry a
  3283 parameter prefix any longer.  INCOMPATIBILITY.
  3284 
  3285 * Class 'instance' command no longer accepts attached definitions.
  3286 INCOMPATIBILITY, use proper 'instantiation' target instead.
  3287 
  3288 * Recovered hiding of consts, which was accidentally broken in
  3289 Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
  3290 makes c inaccessible; consider using ``hide (open) const c'' instead.
  3291 
  3292 * Slightly more coherent Pure syntax, with updated documentation in
  3293 isar-ref manual.  Removed locales meta_term_syntax and
  3294 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
  3295 INCOMPATIBILITY in rare situations.  Note that &&& should not be used
  3296 directly in regular applications.
  3297 
  3298 * There is a new syntactic category "float_const" for signed decimal
  3299 fractions (e.g. 123.45 or -123.45).
  3300 
  3301 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
  3302 interface with 'setup' command instead.
  3303 
  3304 * Command 'local_setup' is similar to 'setup', but operates on a local
  3305 theory context.
  3306 
  3307 * The 'axiomatization' command now only works within a global theory
  3308 context.  INCOMPATIBILITY.
  3309 
  3310 * Goal-directed proof now enforces strict proof irrelevance wrt. sort
  3311 hypotheses.  Sorts required in the course of reasoning need to be
  3312 covered by the constraints in the initial statement, completed by the
  3313 type instance information of the background theory.  Non-trivial sort
  3314 hypotheses, which rarely occur in practice, may be specified via
  3315 vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
  3316 
  3317   lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
  3318 
  3319 The result contains an implicit sort hypotheses as before --
  3320 SORT_CONSTRAINT premises are eliminated as part of the canonical rule
  3321 normalization.
  3322 
  3323 * Generalized Isar history, with support for linear undo, direct state
  3324 addressing etc.
  3325 
  3326 * Changed defaults for unify configuration options:
  3327 
  3328   unify_trace_bound = 50 (formerly 25)
  3329   unify_search_bound = 60 (formerly 30)
  3330 
  3331 * Different bookkeeping for code equations (INCOMPATIBILITY):
  3332 
  3333   a) On theory merge, the last set of code equations for a particular
  3334      constant is taken (in accordance with the policy applied by other
  3335      parts of the code generator framework).
  3336 
  3337   b) Code equations stemming from explicit declarations (e.g. code
  3338      attribute) gain priority over default code equations stemming
  3339      from definition, primrec, fun etc.
  3340 
  3341 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
  3342 
  3343 * Unified theorem tables for both code generators.  Thus [code
  3344 func] has disappeared and only [code] remains.  INCOMPATIBILITY.
  3345 
  3346 * Command 'find_consts' searches for constants based on type and name
  3347 patterns, e.g.
  3348 
  3349     find_consts "_ => bool"
  3350 
  3351 By default, matching is against subtypes, but it may be restricted to
  3352 the whole type.  Searching by name is possible.  Multiple queries are
  3353 conjunctive and queries may be negated by prefixing them with a
  3354 hyphen:
  3355 
  3356     find_consts strict: "_ => bool" name: "Int" -"int => int"
  3357 
  3358 * New 'find_theorems' criterion "solves" matches theorems that
  3359 directly solve the current goal (modulo higher-order unification).
  3360 
  3361 * Auto solve feature for main theorem statements: whenever a new goal
  3362 is stated, "find_theorems solves" is called; any theorems that could
  3363 solve the lemma directly are listed as part of the goal state.
  3364 Cf. associated options in Proof General Isabelle settings menu,
  3365 enabled by default, with reasonable timeout for pathological cases of
  3366 higher-order unification.
  3367 
  3368 
  3369 *** Document preparation ***
  3370 
  3371 * Antiquotation @{lemma} now imitates a regular terminal proof,
  3372 demanding keyword 'by' and supporting the full method expression
  3373 syntax just like the Isar command 'by'.
  3374 
  3375 
  3376 *** HOL ***
  3377 
  3378 * Integrated main parts of former image HOL-Complex with HOL.  Entry
  3379 points Main and Complex_Main remain as before.
  3380 
  3381 * Logic image HOL-Plain provides a minimal HOL with the most important
  3382 tools available (inductive, datatype, primrec, ...).  This facilitates
  3383 experimentation and tool development.  Note that user applications
  3384 (and library theories) should never refer to anything below theory
  3385 Main, as before.
  3386 
  3387 * Logic image HOL-Main stops at theory Main, and thus facilitates
  3388 experimentation due to shorter build times.
  3389 
  3390 * Logic image HOL-NSA contains theories of nonstandard analysis which
  3391 were previously part of former HOL-Complex.  Entry point Hyperreal
  3392 remains valid, but theories formerly using Complex_Main should now use
  3393 new entry point Hypercomplex.
  3394 
  3395 * Generic ATP manager for Sledgehammer, based on ML threads instead of
  3396 Posix processes.  Avoids potentially expensive forking of the ML
  3397 process.  New thread-based implementation also works on non-Unix
  3398 platforms (Cygwin).  Provers are no longer hardwired, but defined
  3399 within the theory via plain ML wrapper functions.  Basic Sledgehammer
  3400 commands are covered in the isar-ref manual.
  3401 
  3402 * Wrapper scripts for remote SystemOnTPTP service allows to use
  3403 sledgehammer without local ATP installation (Vampire etc.). Other
  3404 provers may be included via suitable ML wrappers, see also
  3405 src/HOL/ATP_Linkup.thy.
  3406 
  3407 * ATP selection (E/Vampire/Spass) is now via Proof General's settings
  3408 menu.
  3409 
  3410 * The metis method no longer fails because the theorem is too trivial
  3411 (contains the empty clause).
  3412 
  3413 * The metis method now fails in the usual manner, rather than raising
  3414 an exception, if it determines that it cannot prove the theorem.
  3415 
  3416 * Method "coherent" implements a prover for coherent logic (see also
  3417 src/Tools/coherent.ML).
  3418 
  3419 * Constants "undefined" and "default" replace "arbitrary".  Usually
  3420 "undefined" is the right choice to replace "arbitrary", though
  3421 logically there is no difference.  INCOMPATIBILITY.
  3422 
  3423 * Command "value" now integrates different evaluation mechanisms.  The
  3424 result of the first successful evaluation mechanism is printed.  In
  3425 square brackets a particular named evaluation mechanisms may be
  3426 specified (currently, [SML], [code] or [nbe]).  See further
  3427 src/HOL/ex/Eval_Examples.thy.
  3428 
  3429 * Normalization by evaluation now allows non-leftlinear equations.
  3430 Declare with attribute [code nbe].
  3431 
  3432 * Methods "case_tac" and "induct_tac" now refer to the very same rules
  3433 as the structured Isar versions "cases" and "induct", cf. the
  3434 corresponding "cases" and "induct" attributes.  Mutual induction rules
  3435 are now presented as a list of individual projections
  3436 (e.g. foo_bar.inducts for types foo and bar); the old format with
  3437 explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
  3438 rare situations a different rule is selected --- notably nested tuple
  3439 elimination instead of former prod.exhaust: use explicit (case_tac t
  3440 rule: prod.exhaust) here.
  3441 
  3442 * Attributes "cases", "induct", "coinduct" support "del" option.
  3443 
  3444 * Removed fact "case_split_thm", which duplicates "case_split".
  3445 
  3446 * The option datatype has been moved to a new theory Option.  Renamed
  3447 option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.
  3448 
  3449 * New predicate "strict_mono" classifies strict functions on partial
  3450 orders.  With strict functions on linear orders, reasoning about
  3451 (in)equalities is facilitated by theorems "strict_mono_eq",
  3452 "strict_mono_less_eq" and "strict_mono_less".
  3453 
  3454 * Some set operations are now proper qualified constants with
  3455 authentic syntax.  INCOMPATIBILITY:
  3456 
  3457     op Int ~>   Set.Int
  3458     op Un ~>    Set.Un
  3459     INTER ~>    Set.INTER
  3460     UNION ~>    Set.UNION
  3461     Inter ~>    Set.Inter
  3462     Union ~>    Set.Union
  3463     {} ~>       Set.empty
  3464     UNIV ~>     Set.UNIV
  3465 
  3466 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in
  3467 theory Set.
  3468 
  3469 * Auxiliary class "itself" has disappeared -- classes without any
  3470 parameter are treated as expected by the 'class' command.
  3471 
  3472 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
  3473 
  3474 * Common decision procedures (Cooper, MIR, Ferrack, Approximation,
  3475 Dense_Linear_Order) are now in directory HOL/Decision_Procs.
  3476 
  3477 * Theory src/HOL/Decision_Procs/Approximation provides the new proof
  3478 method "approximation".  It proves formulas on real values by using
  3479 interval arithmetic.  In the formulas are also the transcendental
  3480 functions sin, cos, tan, atan, ln, exp and the constant pi are
  3481 allowed. For examples see
  3482 src/HOL/Descision_Procs/ex/Approximation_Ex.thy.
  3483 
  3484 * Theory "Reflection" now resides in HOL/Library.
  3485 
  3486 * Entry point to Word library now simply named "Word".
  3487 INCOMPATIBILITY.
  3488 
  3489 * Made source layout more coherent with logical distribution
  3490 structure:
  3491 
  3492     src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy
  3493     src/HOL/Library/Code_Message.thy ~> src/HOL/
  3494     src/HOL/Library/GCD.thy ~> src/HOL/
  3495     src/HOL/Library/Order_Relation.thy ~> src/HOL/
  3496     src/HOL/Library/Parity.thy ~> src/HOL/
  3497     src/HOL/Library/Univ_Poly.thy ~> src/HOL/
  3498     src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/
  3499     src/HOL/Real/Lubs.thy ~> src/HOL/
  3500     src/HOL/Real/PReal.thy ~> src/HOL/
  3501     src/HOL/Real/Rational.thy ~> src/HOL/
  3502     src/HOL/Real/RComplete.thy ~> src/HOL/
  3503     src/HOL/Real/RealDef.thy ~> src/HOL/
  3504     src/HOL/Real/RealPow.thy ~> src/HOL/
  3505     src/HOL/Real/Real.thy ~> src/HOL/
  3506     src/HOL/Complex/Complex_Main.thy ~> src/HOL/
  3507     src/HOL/Complex/Complex.thy ~> src/HOL/
  3508     src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/
  3509     src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/
  3510     src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
  3511     src/HOL/Hyperreal/Fact.thy ~> src/HOL/
  3512     src/HOL/Hyperreal/Integration.thy ~> src/HOL/
  3513     src/HOL/Hyperreal/Lim.thy ~> src/HOL/
  3514     src/HOL/Hyperreal/Ln.thy ~> src/HOL/
  3515     src/HOL/Hyperreal/Log.thy ~> src/HOL/
  3516     src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/
  3517     src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/
  3518     src/HOL/Hyperreal/Series.thy ~> src/HOL/
  3519     src/HOL/Hyperreal/SEQ.thy ~> src/HOL/
  3520     src/HOL/Hyperreal/Taylor.thy ~> src/HOL/
  3521     src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/
  3522     src/HOL/Real/Float ~> src/HOL/Library/
  3523     src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach
  3524     src/HOL/Real/RealVector.thy ~> src/HOL/
  3525 
  3526     src/HOL/arith_data.ML ~> src/HOL/Tools
  3527     src/HOL/hologic.ML ~> src/HOL/Tools
  3528     src/HOL/simpdata.ML ~> src/HOL/Tools
  3529     src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML
  3530     src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools
  3531     src/HOL/nat_simprocs.ML ~> src/HOL/Tools
  3532     src/HOL/Real/float_arith.ML ~> src/HOL/Tools
  3533     src/HOL/Real/float_syntax.ML ~> src/HOL/Tools
  3534     src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
  3535     src/HOL/Real/real_arith.ML ~> src/HOL/Tools
  3536 
  3537     src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
  3538     src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
  3539     src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
  3540     src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
  3541     src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
  3542     src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
  3543 
  3544 * If methods "eval" and "evaluation" encounter a structured proof
  3545 state with !!/==>, only the conclusion is evaluated to True (if
  3546 possible), avoiding strange error messages.
  3547 
  3548 * Method "sizechange" automates termination proofs using (a
  3549 modification of) the size-change principle.  Requires SAT solver.  See
  3550 src/HOL/ex/Termination.thy for examples.
  3551 
  3552 * Simplifier: simproc for let expressions now unfolds if bound
  3553 variable occurs at most once in let expression body.  INCOMPATIBILITY.
  3554 
  3555 * Method "arith": Linear arithmetic now ignores all inequalities when
  3556 fast_arith_neq_limit is exceeded, instead of giving up entirely.
  3557 
  3558 * New attribute "arith" for facts that should always be used
  3559 automatically by arithmetic. It is intended to be used locally in
  3560 proofs, e.g.
  3561 
  3562   assumes [arith]: "x > 0"
  3563 
  3564 Global usage is discouraged because of possible performance impact.
  3565 
  3566 * New classes "top" and "bot" with corresponding operations "top" and
  3567 "bot" in theory Orderings; instantiation of class "complete_lattice"
  3568 requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.
  3569 
  3570 * Changed definition lemma "less_fun_def" in order to provide an
  3571 instance for preorders on functions; use lemma "less_le" instead.
  3572 INCOMPATIBILITY.
  3573 
  3574 * Theory Orderings: class "wellorder" moved here, with explicit
  3575 induction rule "less_induct" as assumption.  For instantiation of
  3576 "wellorder" by means of predicate "wf", use rule wf_wellorderI.
  3577 INCOMPATIBILITY.
  3578 
  3579 * Theory Orderings: added class "preorder" as superclass of "order".
  3580 INCOMPATIBILITY: Instantiation proofs for order, linorder
  3581 etc. slightly changed.  Some theorems named order_class.* now named
  3582 preorder_class.*.
  3583 
  3584 * Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,
  3585 "diag" to "Id_on".
  3586 
  3587 * Theory Finite_Set: added a new fold combinator of type
  3588 
  3589   ('a => 'b => 'b) => 'b => 'a set => 'b
  3590 
  3591 Occasionally this is more convenient than the old fold combinator
  3592 which is now defined in terms of the new one and renamed to
  3593 fold_image.
  3594 
  3595 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"
  3596 and "ring_simps" have been replaced by "algebra_simps" (which can be
  3597 extended with further lemmas!).  At the moment both still exist but
  3598 the former will disappear at some point.
  3599 
  3600 * Theory Power: Lemma power_Suc is now declared as a simp rule in
  3601 class recpower.  Type-specific simp rules for various recpower types
  3602 have been removed.  INCOMPATIBILITY, rename old lemmas as follows:
  3603 
  3604 rat_power_0    -> power_0
  3605 rat_power_Suc  -> power_Suc
  3606 realpow_0      -> power_0
  3607 realpow_Suc    -> power_Suc
  3608 complexpow_0   -> power_0
  3609 complexpow_Suc -> power_Suc
  3610 power_poly_0   -> power_0
  3611 power_poly_Suc -> power_Suc
  3612 
  3613 * Theories Ring_and_Field and Divides: Definition of "op dvd" has been
  3614 moved to separate class dvd in Ring_and_Field; a couple of lemmas on
  3615 dvd has been generalized to class comm_semiring_1.  Likewise a bunch
  3616 of lemmas from Divides has been generalized from nat to class
  3617 semiring_div.  INCOMPATIBILITY.  This involves the following theorem
  3618 renames resulting from duplicate elimination:
  3619 
  3620     dvd_def_mod ~>          dvd_eq_mod_eq_0
  3621     zero_dvd_iff ~>         dvd_0_left_iff
  3622     dvd_0 ~>                dvd_0_right
  3623     DIVISION_BY_ZERO_DIV ~> div_by_0
  3624     DIVISION_BY_ZERO_MOD ~> mod_by_0
  3625     mult_div ~>             div_mult_self2_is_id
  3626     mult_mod ~>             mod_mult_self2_is_0
  3627 
  3628 * Theory IntDiv: removed many lemmas that are instances of class-based
  3629 generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,
  3630 rename old lemmas as follows:
  3631 
  3632 dvd_diff               -> nat_dvd_diff
  3633 dvd_zminus_iff         -> dvd_minus_iff
  3634 mod_add1_eq            -> mod_add_eq
  3635 mod_mult1_eq           -> mod_mult_right_eq
  3636 mod_mult1_eq'          -> mod_mult_left_eq
  3637 mod_mult_distrib_mod   -> mod_mult_eq
  3638 nat_mod_add_left_eq    -> mod_add_left_eq
  3639 nat_mod_add_right_eq   -> mod_add_right_eq
  3640 nat_mod_div_trivial    -> mod_div_trivial
  3641 nat_mod_mod_trivial    -> mod_mod_trivial
  3642 zdiv_zadd_self1        -> div_add_self1
  3643 zdiv_zadd_self2        -> div_add_self2
  3644 zdiv_zmult_self1       -> div_mult_self2_is_id
  3645 zdiv_zmult_self2       -> div_mult_self1_is_id
  3646 zdvd_triv_left         -> dvd_triv_left
  3647 zdvd_triv_right        -> dvd_triv_right
  3648 zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
  3649 zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]
  3650 zmod_zadd_left_eq      -> mod_add_left_eq
  3651 zmod_zadd_right_eq     -> mod_add_right_eq
  3652 zmod_zadd_self1        -> mod_add_self1
  3653 zmod_zadd_self2        -> mod_add_self2
  3654 zmod_zadd1_eq          -> mod_add_eq
  3655 zmod_zdiff1_eq         -> mod_diff_eq
  3656 zmod_zdvd_zmod         -> mod_mod_cancel
  3657 zmod_zmod_cancel       -> mod_mod_cancel
  3658 zmod_zmult_self1       -> mod_mult_self2_is_0
  3659 zmod_zmult_self2       -> mod_mult_self1_is_0
  3660 zmod_1                 -> mod_by_1
  3661 zdiv_1                 -> div_by_1
  3662 zdvd_abs1              -> abs_dvd_iff
  3663 zdvd_abs2              -> dvd_abs_iff
  3664 zdvd_refl              -> dvd_refl
  3665 zdvd_trans             -> dvd_trans
  3666 zdvd_zadd              -> dvd_add
  3667 zdvd_zdiff             -> dvd_diff
  3668 zdvd_zminus_iff        -> dvd_minus_iff
  3669 zdvd_zminus2_iff       -> minus_dvd_iff
  3670 zdvd_zmultD            -> dvd_mult_right
  3671 zdvd_zmultD2           -> dvd_mult_left
  3672 zdvd_zmult_mono        -> mult_dvd_mono
  3673 zdvd_0_right           -> dvd_0_right
  3674 zdvd_0_left            -> dvd_0_left_iff
  3675 zdvd_1_left            -> one_dvd
  3676 zminus_dvd_iff         -> minus_dvd_iff
  3677 
  3678 * Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
  3679 
  3680 * The real numbers offer decimal input syntax: 12.34 is translated
  3681 into 1234/10^2. This translation is not reversed upon output.
  3682 
  3683 * Theory Library/Polynomial defines an abstract type 'a poly of
  3684 univariate polynomials with coefficients of type 'a.  In addition to
  3685 the standard ring operations, it also supports div and mod.  Code
  3686 generation is also supported, using list-style constructors.
  3687 
  3688 * Theory Library/Inner_Product defines a class of real_inner for real
  3689 inner product spaces, with an overloaded operation inner :: 'a => 'a
  3690 => real.  Class real_inner is a subclass of real_normed_vector from
  3691 theory RealVector.
  3692 
  3693 * Theory Library/Product_Vector provides instances for the product
  3694 type 'a * 'b of several classes from RealVector and Inner_Product.
  3695 Definitions of addition, subtraction, scalar multiplication, norms,
  3696 and inner products are included.
  3697 
  3698 * Theory Library/Bit defines the field "bit" of integers modulo 2.  In
  3699 addition to the field operations, numerals and case syntax are also
  3700 supported.
  3701 
  3702 * Theory Library/Diagonalize provides constructive version of Cantor's
  3703 first diagonalization argument.
  3704 
  3705 * Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
  3706 zlcm (for int); carried together from various gcd/lcm developements in
  3707 the HOL Distribution.  Constants zgcd and zlcm replace former igcd and
  3708 ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,
  3709 may recover tupled syntax as follows:
  3710 
  3711     hide (open) const gcd
  3712     abbreviation gcd where
  3713       "gcd == (%(a, b). GCD.gcd a b)"
  3714     notation (output)
  3715       GCD.gcd ("gcd '(_, _')")
  3716 
  3717 The same works for lcm, zgcd, zlcm.
  3718 
  3719 * Theory Library/Nat_Infinity: added addition, numeral syntax and more
  3720 instantiations for algebraic structures.  Removed some duplicate
  3721 theorems.  Changes in simp rules.  INCOMPATIBILITY.
  3722 
  3723 * ML antiquotation @{code} takes a constant as argument and generates
  3724 corresponding code in background and inserts name of the corresponding
  3725 resulting ML value/function/datatype constructor binding in place.
  3726 All occurrences of @{code} with a single ML block are generated
  3727 simultaneously.  Provides a generic and safe interface for
  3728 instrumentalizing code generation.  See
  3729 src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.
  3730 In future you ought to refrain from ad-hoc compiling generated SML
  3731 code on the ML toplevel.  Note that (for technical reasons) @{code}
  3732 cannot refer to constants for which user-defined serializations are
  3733 set.  Refer to the corresponding ML counterpart directly in that
  3734 cases.
  3735 
  3736 * Command 'rep_datatype': instead of theorem names the command now
  3737 takes a list of terms denoting the constructors of the type to be
  3738 represented as datatype.  The characteristic theorems have to be
  3739 proven.  INCOMPATIBILITY.  Also observe that the following theorems
  3740 have disappeared in favour of existing ones:
  3741 
  3742     unit_induct                 ~> unit.induct
  3743     prod_induct                 ~> prod.induct
  3744     sum_induct                  ~> sum.induct
  3745     Suc_Suc_eq                  ~> nat.inject
  3746     Suc_not_Zero Zero_not_Suc   ~> nat.distinct
  3747 
  3748 
  3749 *** HOL-Algebra ***
  3750 
  3751 * New locales for orders and lattices where the equivalence relation
  3752 is not restricted to equality.  INCOMPATIBILITY: all order and lattice
  3753 locales use a record structure with field eq for the equivalence.
  3754 
  3755 * New theory of factorial domains.
  3756 
  3757 * Units_l_inv and Units_r_inv are now simp rules by default.
  3758 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
  3759 and/or r_inv will now also require deletion of these lemmas.
  3760 
  3761 * Renamed the following theorems, INCOMPATIBILITY:
  3762 
  3763 UpperD ~> Upper_memD
  3764 LowerD ~> Lower_memD
  3765 least_carrier ~> least_closed
  3766 greatest_carrier ~> greatest_closed
  3767 greatest_Lower_above ~> greatest_Lower_below
  3768 one_zero ~> carrier_one_zero
  3769 one_not_zero ~> carrier_one_not_zero  (collision with assumption)
  3770 
  3771 
  3772 *** HOL-Nominal ***
  3773 
  3774 * Nominal datatypes can now contain type-variables.
  3775 
  3776 * Commands 'nominal_inductive' and 'equivariance' work with local
  3777 theory targets.
  3778 
  3779 * Nominal primrec can now works with local theory targets and its
  3780 specification syntax now conforms to the general format as seen in
  3781 'inductive' etc.
  3782 
  3783 * Method "perm_simp" honours the standard simplifier attributes
  3784 (no_asm), (no_asm_use) etc.
  3785 
  3786 * The new predicate #* is defined like freshness, except that on the
  3787 left hand side can be a set or list of atoms.
  3788 
  3789 * Experimental command 'nominal_inductive2' derives strong induction
  3790 principles for inductive definitions.  In contrast to
  3791 'nominal_inductive', which can only deal with a fixed number of
  3792 binders, it can deal with arbitrary expressions standing for sets of
  3793 atoms to be avoided.  The only inductive definition we have at the
  3794 moment that needs this generalisation is the typing rule for Lets in
  3795 the algorithm W:
  3796 
  3797  Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
  3798  -----------------------------------------------------------------
  3799          Gamma |- Let x be t1 in t2 : T2
  3800 
  3801 In this rule one wants to avoid all the binders that are introduced by
  3802 "close Gamma T1".  We are looking for other examples where this
  3803 feature might be useful.  Please let us know.
  3804 
  3805 
  3806 *** HOLCF ***
  3807 
  3808 * Reimplemented the simplification procedure for proving continuity
  3809 subgoals.  The new simproc is extensible; users can declare additional
  3810 continuity introduction rules with the attribute [cont2cont].
  3811 
  3812 * The continuity simproc now uses a different introduction rule for
  3813 solving continuity subgoals on terms with lambda abstractions.  In
  3814 some rare cases the new simproc may fail to solve subgoals that the
  3815 old one could solve, and "simp add: cont2cont_LAM" may be necessary.
  3816 Potential INCOMPATIBILITY.
  3817 
  3818 * Command 'fixrec': specification syntax now conforms to the general
  3819 format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
  3820 examples.  INCOMPATIBILITY.
  3821 
  3822 
  3823 *** ZF ***
  3824 
  3825 * Proof of Zorn's Lemma for partial orders.
  3826 
  3827 
  3828 *** ML ***
  3829 
  3830 * Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
  3831 Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility
  3832 depends on multithreading, so timouts will not work before Poly/ML
  3833 5.2.1!
  3834 
  3835 * High-level support for concurrent ML programming, see
  3836 src/Pure/Cuncurrent.  The data-oriented model of "future values" is
  3837 particularly convenient to organize independent functional
  3838 computations.  The concept of "synchronized variables" provides a
  3839 higher-order interface for components with shared state, avoiding the
  3840 delicate details of mutexes and condition variables.  (Requires
  3841 Poly/ML 5.2.1 or later.)
  3842 
  3843 * ML bindings produced via Isar commands are stored within the Isar
  3844 context (theory or proof).  Consequently, commands like 'use' and 'ML'
  3845 become thread-safe and work with undo as expected (concerning
  3846 top-level bindings, not side-effects on global references).
  3847 INCOMPATIBILITY, need to provide proper Isar context when invoking the
  3848 compiler at runtime; really global bindings need to be given outside a
  3849 theory.  (Requires Poly/ML 5.2 or later.)
  3850 
  3851 * Command 'ML_prf' is analogous to 'ML' but works within a proof
  3852 context.  Top-level ML bindings are stored within the proof context in
  3853 a purely sequential fashion, disregarding the nested proof structure.
  3854 ML bindings introduced by 'ML_prf' are discarded at the end of the
  3855 proof.  (Requires Poly/ML 5.2 or later.)
  3856 
  3857 * Simplified ML attribute and method setup, cf. functions Attrib.setup
  3858 and Method.setup, as well as Isar commands 'attribute_setup' and
  3859 'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify
  3860 existing code accordingly, or use plain 'setup' together with old
  3861 Method.add_method.
  3862 
  3863 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
  3864 to 'a -> thm, while results are always tagged with an authentic oracle
  3865 name.  The Isar command 'oracle' is now polymorphic, no argument type
  3866 is specified.  INCOMPATIBILITY, need to simplify existing oracle code
  3867 accordingly.  Note that extra performance may be gained by producing
  3868 the cterm carefully, avoiding slow Thm.cterm_of.
  3869 
  3870 * Simplified interface for defining document antiquotations via
  3871 ThyOutput.antiquotation, ThyOutput.output, and optionally
  3872 ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
  3873 antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
  3874 examples.
  3875 
  3876 * More systematic treatment of long names, abstract name bindings, and
  3877 name space operations.  Basic operations on qualified names have been
  3878 move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
  3879 Long_Name.append.  Old type bstring has been mostly replaced by
  3880 abstract type binding (see structure Binding), which supports precise
  3881 qualification by packages and local theory targets, as well as proper
  3882 tracking of source positions.  INCOMPATIBILITY, need to wrap old
  3883 bstring values into Binding.name, or better pass through abstract
  3884 bindings everywhere.  See further src/Pure/General/long_name.ML,
  3885 src/Pure/General/binding.ML and src/Pure/General/name_space.ML
  3886 
  3887 * Result facts (from PureThy.note_thms, ProofContext.note_thms,
  3888 LocalTheory.note etc.) now refer to the *full* internal name, not the
  3889 bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!
  3890 
  3891 * Disposed old type and term read functions (Sign.read_def_typ,
  3892 Sign.read_typ, Sign.read_def_terms, Sign.read_term,
  3893 Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should
  3894 use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,
  3895 Syntax.read_term_global etc.; see also OldGoals.read_term as last
  3896 resort for legacy applications.
  3897 
  3898 * Disposed old declarations, tactics, tactic combinators that refer to
  3899 the simpset or claset of an implicit theory (such as Addsimps,
  3900 Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in
  3901 embedded ML text, or local_simpset_of with a proper context passed as
  3902 explicit runtime argument.
  3903 
  3904 * Rules and tactics that read instantiations (read_instantiate,
  3905 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
  3906 context, which is required for parsing and type-checking.  Moreover,
  3907 the variables are specified as plain indexnames, not string encodings
  3908 thereof.  INCOMPATIBILITY.
  3909 
  3910 * Generic Toplevel.add_hook interface allows to analyze the result of
  3911 transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
  3912 for theorem dependency output of transactions resulting in a new
  3913 theory state.
  3914 
  3915 * ML antiquotations: block-structured compilation context indicated by
  3916 \<lbrace> ... \<rbrace>; additional antiquotation forms:
  3917 
  3918   @{binding name}                         - basic name binding
  3919   @{let ?pat = term}                      - term abbreviation (HO matching)
  3920   @{note name = fact}                     - fact abbreviation
  3921   @{thm fact}                             - singleton fact (with attributes)
  3922   @{thms fact}                            - general fact (with attributes)
  3923   @{lemma prop by method}                 - singleton goal
  3924   @{lemma prop by meth1 meth2}            - singleton goal
  3925   @{lemma prop1 ... propN by method}      - general goal
  3926   @{lemma prop1 ... propN by meth1 meth2} - general goal
  3927   @{lemma (open) ...}                     - open derivation
  3928 
  3929 
  3930 *** System ***
  3931 
  3932 * The Isabelle "emacs" tool provides a specific interface to invoke
  3933 Proof General / Emacs, with more explicit failure if that is not
  3934 installed (the old isabelle-interface script silently falls back on
  3935 isabelle-process).  The PROOFGENERAL_HOME setting determines the
  3936 installation location of the Proof General distribution.
  3937 
  3938 * Isabelle/lib/classes/Pure.jar provides basic support to integrate
  3939 the Isabelle process into a JVM/Scala application.  See
  3940 Isabelle/lib/jedit/plugin for a minimal example.  (The obsolete Java
  3941 process wrapper has been discontinued.)
  3942 
  3943 * Added homegrown Isabelle font with unicode layout, see lib/fonts.
  3944 
  3945 * Various status messages (with exact source position information) are
  3946 emitted, if proper markup print mode is enabled.  This allows
  3947 user-interface components to provide detailed feedback on internal
  3948 prover operations.
  3949 
  3950 
  3951 
  3952 New in Isabelle2008 (June 2008)
  3953 -------------------------------
  3954 
  3955 *** General ***
  3956 
  3957 * The Isabelle/Isar Reference Manual (isar-ref) has been reorganized
  3958 and updated, with formally checked references as hyperlinks.
  3959 
  3960 * Theory loader: use_thy (and similar operations) no longer set the
  3961 implicit ML context, which was occasionally hard to predict and in
  3962 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
  3963 provides a proper context already.
  3964 
  3965 * Theory loader: old-style ML proof scripts being *attached* to a thy
  3966 file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
  3967 'use' within a theory file will do the job.
  3968 
  3969 * Name space merge now observes canonical order, i.e. the second space
  3970 is inserted into the first one, while existing entries in the first
  3971 space take precedence.  INCOMPATIBILITY in rare situations, may try to
  3972 swap theory imports.
  3973 
  3974 * Syntax: symbol \<chi> is now considered a letter.  Potential
  3975 INCOMPATIBILITY in identifier syntax etc.
  3976 
  3977 * Outer syntax: string tokens no longer admit escaped white space,
  3978 which was an accidental (undocumented) feature.  INCOMPATIBILITY, use
  3979 white space without escapes.
  3980 
  3981 * Outer syntax: string tokens may contain arbitrary character codes
  3982 specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
  3983 "foo_bar".
  3984 
  3985 
  3986 *** Pure ***
  3987 
  3988 * Context-dependent token translations.  Default setup reverts locally
  3989 fixed variables, and adds hilite markup for undeclared frees.
  3990 
  3991 * Unused theorems can be found using the new command 'unused_thms'.
  3992 There are three ways of invoking it:
  3993 
  3994 (1) unused_thms
  3995      Only finds unused theorems in the current theory.
  3996 
  3997 (2) unused_thms thy_1 ... thy_n -
  3998      Finds unused theorems in the current theory and all of its ancestors,
  3999      excluding the theories thy_1 ... thy_n and all of their ancestors.
  4000 
  4001 (3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m
  4002      Finds unused theorems in the theories thy'_1 ... thy'_m and all of
  4003      their ancestors, excluding the theories thy_1 ... thy_n and all of
  4004      their ancestors.
  4005 
  4006 In order to increase the readability of the list produced by
  4007 unused_thms, theorems that have been created by a particular instance
  4008 of a theory command such as 'inductive' or 'function' are considered
  4009 to belong to the same "group", meaning that if at least one theorem in
  4010 this group is used, the other theorems in the same group are no longer
  4011 reported as unused.  Moreover, if all theorems in the group are
  4012 unused, only one theorem in the group is displayed.
  4013 
  4014 Note that proof objects have to be switched on in order for
  4015 unused_thms to work properly (i.e. !proofs must be >= 1, which is
  4016 usually the case when using Proof General with the default settings).
  4017 
  4018 * Authentic naming of facts disallows ad-hoc overwriting of previous
  4019 theorems within the same name space.  INCOMPATIBILITY, need to remove
  4020 duplicate fact bindings, or even accidental fact duplications.  Note
  4021 that tools may maintain dynamically scoped facts systematically, using
  4022 PureThy.add_thms_dynamic.
  4023 
  4024 * Command 'hide' now allows to hide from "fact" name space as well.
  4025 
  4026 * Eliminated destructive theorem database, simpset, claset, and
  4027 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
  4028 update of theories within ML code.
  4029 
  4030 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
  4031 INCOMPATIBILITY, object-logics depending on former Pure require
  4032 additional setup PureThy.old_appl_syntax_setup; object-logics
  4033 depending on former CPure need to refer to Pure.
  4034 
  4035 * Commands 'use' and 'ML' are now purely functional, operating on
  4036 theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
  4037 instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
  4038 INCOMPATIBILITY.
  4039 
  4040 * Command 'setup': discontinued implicit version with ML reference.
  4041 
  4042 * Instantiation target allows for simultaneous specification of class
  4043 instance operations together with an instantiation proof.
  4044 Type-checking phase allows to refer to class operations uniformly.
  4045 See src/HOL/Complex/Complex.thy for an Isar example and
  4046 src/HOL/Library/Eval.thy for an ML example.
  4047 
  4048 * Indexing of literal facts: be more serious about including only
  4049 facts from the visible specification/proof context, but not the
  4050 background context (locale etc.).  Affects `prop` notation and method
  4051 "fact".  INCOMPATIBILITY: need to name facts explicitly in rare
  4052 situations.
  4053 
  4054 * Method "cases", "induct", "coinduct": removed obsolete/undocumented
  4055 "(open)" option, which used to expose internal bound variables to the
  4056 proof text.
  4057 
  4058 * Isar statements: removed obsolete case "rule_context".
  4059 INCOMPATIBILITY, better use explicit fixes/assumes.
  4060 
  4061 * Locale proofs: default proof step now includes 'unfold_locales';
  4062 hence 'proof' without argument may be used to unfold locale
  4063 predicates.
  4064 
  4065 
  4066 *** Document preparation ***
  4067 
  4068 * Simplified pdfsetup.sty: color/hyperref is used unconditionally for
  4069 both pdf and dvi (hyperlinks usually work in xdvi as well); removed
  4070 obsolete thumbpdf setup (contemporary PDF viewers do this on the
  4071 spot); renamed link color from "darkblue" to "linkcolor" (default
  4072 value unchanged, can be redefined via \definecolor); no longer sets
  4073 "a4paper" option (unnecessary or even intrusive).
  4074 
  4075 * Antiquotation @{lemma A method} proves proposition A by the given
  4076 method (either a method name or a method name plus (optional) method
  4077 arguments in parentheses) and prints A just like @{prop A}.
  4078 
  4079 
  4080 *** HOL ***
  4081 
  4082 * New primrec package.  Specification syntax conforms in style to
  4083 definition/function/....  No separate induction rule is provided.  The
  4084 "primrec" command distinguishes old-style and new-style specifications
  4085 by syntax.  The former primrec package is now named OldPrimrecPackage.
  4086 When adjusting theories, beware: constants stemming from new-style
  4087 primrec specifications have authentic syntax.
  4088 
  4089 * Metis prover is now an order of magnitude faster, and also works
  4090 with multithreading.
  4091 
  4092 * Metis: the maximum number of clauses that can be produced from a
  4093 theorem is now given by the attribute max_clauses.  Theorems that
  4094 exceed this number are ignored, with a warning printed.
  4095 
  4096 * Sledgehammer no longer produces structured proofs by default. To
  4097 enable, declare [[sledgehammer_full = true]].  Attributes
  4098 reconstruction_modulus, reconstruction_sorts renamed
  4099 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
  4100 
  4101 * Method "induct_scheme" derives user-specified induction rules
  4102 from well-founded induction and completeness of patterns. This factors
  4103 out some operations that are done internally by the function package
  4104 and makes them available separately.  See
  4105 src/HOL/ex/Induction_Scheme.thy for examples.
  4106 
  4107 * More flexible generation of measure functions for termination
  4108 proofs: Measure functions can be declared by proving a rule of the
  4109 form "is_measure f" and giving it the [measure_function] attribute.
  4110 The "is_measure" predicate is logically meaningless (always true), and
  4111 just guides the heuristic.  To find suitable measure functions, the
  4112 termination prover sets up the goal "is_measure ?f" of the appropriate
  4113 type and generates all solutions by prolog-style backwards proof using
  4114 the declared rules.
  4115 
  4116 This setup also deals with rules like 
  4117 
  4118   "is_measure f ==> is_measure (list_size f)"
  4119 
  4120 which accommodates nested datatypes that recurse through lists.
  4121 Similar rules are predeclared for products and option types.
  4122 
  4123 * Turned the type of sets "'a set" into an abbreviation for "'a => bool"
  4124 
  4125   INCOMPATIBILITIES:
  4126 
  4127   - Definitions of overloaded constants on sets have to be replaced by
  4128     definitions on => and bool.
  4129 
  4130   - Some definitions of overloaded operators on sets can now be proved
  4131     using the definitions of the operators on => and bool.  Therefore,
  4132     the following theorems have been renamed:
  4133 
  4134       subset_def   -> subset_eq
  4135       psubset_def  -> psubset_eq
  4136       set_diff_def -> set_diff_eq
  4137       Compl_def    -> Compl_eq
  4138       Sup_set_def  -> Sup_set_eq
  4139       Inf_set_def  -> Inf_set_eq
  4140       sup_set_def  -> sup_set_eq
  4141       inf_set_def  -> inf_set_eq
  4142 
  4143   - Due to the incompleteness of the HO unification algorithm, some
  4144     rules such as subst may require manual instantiation, if some of
  4145     the unknowns in the rule is a set.
  4146 
  4147   - Higher order unification and forward proofs:
  4148     The proof pattern
  4149 
  4150       have "P (S::'a set)" <...>
  4151       then have "EX S. P S" ..
  4152 
  4153     no longer works (due to the incompleteness of the HO unification
  4154     algorithm) and must be replaced by the pattern
  4155 
  4156       have "EX S. P S"
  4157       proof
  4158         show "P S" <...>
  4159       qed
  4160 
  4161   - Calculational reasoning with subst (or similar rules):
  4162     The proof pattern
  4163 
  4164       have "P (S::'a set)" <...>
  4165       also have "S = T" <...>
  4166       finally have "P T" .
  4167 
  4168     no longer works (for similar reasons as the previous example) and
  4169     must be replaced by something like
  4170 
  4171       have "P (S::'a set)" <...>
  4172       moreover have "S = T" <...>
  4173       ultimately have "P T" by simp
  4174 
  4175   - Tactics or packages written in ML code:
  4176     Code performing pattern matching on types via
  4177 
  4178       Type ("set", [T]) => ...
  4179 
  4180     must be rewritten. Moreover, functions like strip_type or
  4181     binder_types no longer return the right value when applied to a
  4182     type of the form
  4183 
  4184       T1 => ... => Tn => U => bool
  4185 
  4186     rather than
  4187 
  4188       T1 => ... => Tn => U set
  4189 
  4190 * Merged theories Wellfounded_Recursion, Accessible_Part and
  4191 Wellfounded_Relations to theory Wellfounded.
  4192 
  4193 * Explicit class "eq" for executable equality.  INCOMPATIBILITY.
  4194 
  4195 * Class finite no longer treats UNIV as class parameter.  Use class
  4196 enum from theory Library/Enum instead to achieve a similar effect.
  4197 INCOMPATIBILITY.
  4198 
  4199 * Theory List: rule list_induct2 now has explicitly named cases "Nil"
  4200 and "Cons".  INCOMPATIBILITY.
  4201 
  4202 * HOL (and FOL): renamed variables in rules imp_elim and swap.
  4203 Potential INCOMPATIBILITY.
  4204 
  4205 * Theory Product_Type: duplicated lemmas split_Pair_apply and
  4206 injective_fst_snd removed, use split_eta and prod_eqI instead.
  4207 Renamed upd_fst to apfst and upd_snd to apsnd.  INCOMPATIBILITY.
  4208 
  4209 * Theory Nat: removed redundant lemmas that merely duplicate lemmas of
  4210 the same name in theory Orderings:
  4211 
  4212   less_trans
  4213   less_linear
  4214   le_imp_less_or_eq
  4215   le_less_trans
  4216   less_le_trans
  4217   less_not_sym
  4218   less_asym
  4219 
  4220 Renamed less_imp_le to less_imp_le_nat, and less_irrefl to
  4221 less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types
  4222 and different variable names.
  4223 
  4224 * Library/Option_ord.thy: Canonical order on option type.
  4225 
  4226 * Library/RBT.thy: Red-black trees, an efficient implementation of
  4227 finite maps.
  4228 
  4229 * Library/Countable.thy: Type class for countable types.
  4230 
  4231 * Theory Int: The representation of numerals has changed.  The infix
  4232 operator BIT and the bit datatype with constructors B0 and B1 have
  4233 disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
  4234 place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems
  4235 involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"
  4236 accordingly.
  4237 
  4238 * Theory Nat: definition of <= and < on natural numbers no longer
  4239 depend on well-founded relations.  INCOMPATIBILITY.  Definitions
  4240 le_def and less_def have disappeared.  Consider lemmas not_less
  4241 [symmetric, where ?'a = nat] and less_eq [symmetric] instead.
  4242 
  4243 * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
  4244 (whose purpose mainly is for various fold_set functionals) have been
  4245 abandoned in favor of the existing algebraic classes
  4246 ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
  4247 lower_semilattice (resp. upper_semilattice) and linorder.
  4248 INCOMPATIBILITY.
  4249 
  4250 * Theory Transitive_Closure: induct and cases rules now declare proper
  4251 case_names ("base" and "step").  INCOMPATIBILITY.
  4252 
  4253 * Theorem Inductive.lfp_ordinal_induct generalized to complete
  4254 lattices.  The form set-specific version is available as
  4255 Inductive.lfp_ordinal_induct_set.
  4256 
  4257 * Renamed theorems "power.simps" to "power_int.simps".
  4258 INCOMPATIBILITY.
  4259 
  4260 * Class semiring_div provides basic abstract properties of semirings
  4261 with division and modulo operations.  Subsumes former class dvd_mod.
  4262 
  4263 * Merged theories IntDef, Numeral and IntArith into unified theory
  4264 Int.  INCOMPATIBILITY.
  4265 
  4266 * Theory Library/Code_Index: type "index" now represents natural
  4267 numbers rather than integers.  INCOMPATIBILITY.
  4268 
  4269 * New class "uminus" with operation "uminus" (split of from class
  4270 "minus" which now only has operation "minus", binary).
  4271 INCOMPATIBILITY.
  4272 
  4273 * Constants "card", "internal_split", "option_map" now with authentic
  4274 syntax.  INCOMPATIBILITY.
  4275 
  4276 * Definitions subset_def, psubset_def, set_diff_def, Compl_def,
  4277 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
  4278 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
  4279 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
  4280 Sup_set_def, le_def, less_def, option_map_def now with object
  4281 equality.  INCOMPATIBILITY.
  4282 
  4283 * Records. Removed K_record, and replaced it by pure lambda term
  4284 %x. c. The simplifier setup is now more robust against eta expansion.
  4285 INCOMPATIBILITY: in cases explicitly referring to K_record.
  4286 
  4287 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
  4288 
  4289 * Library/ListVector: new theory of arithmetic vector operations.
  4290 
  4291 * Library/Order_Relation: new theory of various orderings as sets of
  4292 pairs.  Defines preorders, partial orders, linear orders and
  4293 well-orders on sets and on types.
  4294 
  4295 
  4296 *** ZF ***
  4297 
  4298 * Renamed some theories to allow to loading both ZF and HOL in the
  4299 same session:
  4300 
  4301   Datatype  -> Datatype_ZF
  4302   Inductive -> Inductive_ZF
  4303   Int       -> Int_ZF
  4304   IntDiv    -> IntDiv_ZF
  4305   Nat       -> Nat_ZF
  4306   List      -> List_ZF
  4307   Main      -> Main_ZF
  4308 
  4309 INCOMPATIBILITY: ZF theories that import individual theories below
  4310 Main might need to be adapted.  Regular theory Main is still
  4311 available, as trivial extension of Main_ZF.
  4312 
  4313 
  4314 *** ML ***
  4315 
  4316 * ML within Isar: antiquotation @{const name} or @{const
  4317 name(typargs)} produces statically-checked Const term.
  4318 
  4319 * Functor NamedThmsFun: data is available to the user as dynamic fact
  4320 (of the same name).  Removed obsolete print command.
  4321 
  4322 * Removed obsolete "use_legacy_bindings" function.
  4323 
  4324 * The ``print mode'' is now a thread-local value derived from a global
  4325 template (the former print_mode reference), thus access becomes
  4326 non-critical.  The global print_mode reference is for session
  4327 management only; user-code should use print_mode_value,
  4328 print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
  4329 
  4330 * Functions system/system_out provide a robust way to invoke external
  4331 shell commands, with propagation of interrupts (requires Poly/ML
  4332 5.2.1).  Do not use OS.Process.system etc. from the basis library!
  4333 
  4334 
  4335 *** System ***
  4336 
  4337 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs ---
  4338 in accordance with Proof General 3.7, which prefers GNU emacs.
  4339 
  4340 * isatool tty runs Isabelle process with plain tty interaction;
  4341 optional line editor may be specified via ISABELLE_LINE_EDITOR
  4342 setting, the default settings attempt to locate "ledit" and "rlwrap".
  4343 
  4344 * isatool browser now works with Cygwin as well, using general
  4345 "javapath" function defined in Isabelle process environment.
  4346 
  4347 * YXML notation provides a simple and efficient alternative to
  4348 standard XML transfer syntax.  See src/Pure/General/yxml.ML and
  4349 isatool yxml as described in the Isabelle system manual.
  4350 
  4351 * JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes)
  4352 provides general wrapper for managing an Isabelle process in a robust
  4353 fashion, with ``cooked'' output from stdin/stderr.
  4354 
  4355 * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit),
  4356 based on Isabelle/JVM process wrapper (see Isabelle/lib/classes).
  4357 
  4358 * Removed obsolete THIS_IS_ISABELLE_BUILD feature.  NB: the documented
  4359 way of changing the user's settings is via
  4360 ISABELLE_HOME_USER/etc/settings, which is a fully featured bash
  4361 script.
  4362 
  4363 * Multithreading.max_threads := 0 refers to the number of actual CPU
  4364 cores of the underlying machine, which is a good starting point for
  4365 optimal performance tuning.  The corresponding usedir option -M allows
  4366 "max" as an alias for "0".  WARNING: does not work on certain versions
  4367 of Mac OS (with Poly/ML 5.1).
  4368 
  4369 * isabelle-process: non-ML sessions are run with "nice", to reduce the
  4370 adverse effect of Isabelle flooding interactive front-ends (notably
  4371 ProofGeneral / XEmacs).
  4372 
  4373 
  4374 
  4375 New in Isabelle2007 (November 2007)
  4376 -----------------------------------
  4377 
  4378 *** General ***
  4379 
  4380 * More uniform information about legacy features, notably a
  4381 warning/error of "Legacy feature: ...", depending on the state of the
  4382 tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY:
  4383 legacy features will disappear eventually.
  4384 
  4385 * Theory syntax: the header format ``theory A = B + C:'' has been
  4386 discontinued in favour of ``theory A imports B C begin''.  Use isatool
  4387 fixheaders to convert existing theory files.  INCOMPATIBILITY.
  4388 
  4389 * Theory syntax: the old non-Isar theory file format has been
  4390 discontinued altogether.  Note that ML proof scripts may still be used
  4391 with Isar theories; migration is usually quite simple with the ML
  4392 function use_legacy_bindings.  INCOMPATIBILITY.
  4393 
  4394 * Theory syntax: some popular names (e.g. 'class', 'declaration',
  4395 'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double
  4396 quotes.
  4397 
  4398 * Theory loader: be more serious about observing the static theory
  4399 header specifications (including optional directories), but not the
  4400 accidental file locations of previously successful loads.  The strict
  4401 update policy of former update_thy is now already performed by
  4402 use_thy, so the former has been removed; use_thys updates several
  4403 theories simultaneously, just as 'imports' within a theory header
  4404 specification, but without merging the results.  Potential
  4405 INCOMPATIBILITY: may need to refine theory headers and commands
  4406 ROOT.ML which depend on load order.
  4407 
  4408 * Theory loader: optional support for content-based file
  4409 identification, instead of the traditional scheme of full physical
  4410 path plus date stamp; configured by the ISABELLE_FILE_IDENT setting
  4411 (cf. the system manual).  The new scheme allows to work with
  4412 non-finished theories in persistent session images, such that source
  4413 files may be moved later on without requiring reloads.
  4414 
  4415 * Theory loader: old-style ML proof scripts being *attached* to a thy
  4416 file (with the same base name as the theory) are considered a legacy
  4417 feature, which will disappear eventually. Even now, the theory loader
  4418 no longer maintains dependencies on such files.
  4419 
  4420 * Syntax: the scope for resolving ambiguities via type-inference is
  4421 now limited to individual terms, instead of whole simultaneous
  4422 specifications as before. This greatly reduces the complexity of the
  4423 syntax module and improves flexibility by separating parsing and
  4424 type-checking. INCOMPATIBILITY: additional type-constraints (explicit
  4425 'fixes' etc.) are required in rare situations.
  4426 
  4427 * Syntax: constants introduced by new-style packages ('definition',
  4428 'abbreviation' etc.) are passed through the syntax module in
  4429 ``authentic mode''. This means that associated mixfix annotations
  4430 really stick to such constants, independently of potential name space
  4431 ambiguities introduced later on. INCOMPATIBILITY: constants in parse
  4432 trees are represented slightly differently, may need to adapt syntax
  4433 translations accordingly. Use CONST marker in 'translations' and
  4434 @{const_syntax} antiquotation in 'parse_translation' etc.
  4435 
  4436 * Legacy goal package: reduced interface to the bare minimum required
  4437 to keep existing proof scripts running.  Most other user-level
  4438 functions are now part of the OldGoals structure, which is *not* open
  4439 by default (consider isatool expandshort before open OldGoals).
  4440 Removed top_sg, prin, printyp, pprint_term/typ altogether, because
  4441 these tend to cause confusion about the actual goal (!) context being
  4442 used here, which is not necessarily the same as the_context().
  4443 
  4444 * Command 'find_theorems': supports "*" wild-card in "name:"
  4445 criterion; "with_dups" option.  Certain ProofGeneral versions might
  4446 support a specific search form (see ProofGeneral/CHANGES).
  4447 
  4448 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
  4449 by default, which means that "prems" (and also "fixed variables") are
  4450 suppressed from proof state output.  Note that the ProofGeneral
  4451 settings mechanism allows to change and save options persistently, but
  4452 older versions of Isabelle will fail to start up if a negative prems
  4453 limit is imposed.
  4454 
  4455 * Local theory targets may be specified by non-nested blocks of
  4456 ``context/locale/class ... begin'' followed by ``end''.  The body may
  4457 contain definitions, theorems etc., including any derived mechanism
  4458 that has been implemented on top of these primitives.  This concept
  4459 generalizes the existing ``theorem (in ...)'' towards more versatility
  4460 and scalability.
  4461 
  4462 * Proof General interface: proper undo of final 'end' command;
  4463 discontinued Isabelle/classic mode (ML proof scripts).
  4464 
  4465 
  4466 *** Document preparation ***
  4467 
  4468 * Added antiquotation @{theory name} which prints the given name,
  4469 after checking that it refers to a valid ancestor theory in the
  4470 current context.
  4471 
  4472 * Added antiquotations @{ML_type text} and @{ML_struct text} which
  4473 check the given source text as ML type/structure, printing verbatim.
  4474 
  4475 * Added antiquotation @{abbrev "c args"} which prints the abbreviation
  4476 "c args == rhs" given in the current context.  (Any number of
  4477 arguments may be given on the LHS.)
  4478 
  4479 
  4480 *** Pure ***
  4481 
  4482 * The 'class' package offers a combination of axclass and locale to
  4483 achieve Haskell-like type classes in Isabelle.  Definitions and
  4484 theorems within a class context produce both relative results (with
  4485 implicit parameters according to the locale context), and polymorphic
  4486 constants with qualified polymorphism (according to the class
  4487 context).  Within the body context of a 'class' target, a separate
  4488 syntax layer ("user space type system") takes care of converting
  4489 between global polymorphic consts and internal locale representation.
  4490 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).
  4491 "isatool doc classes" provides a tutorial.
  4492 
  4493 * Generic code generator framework allows to generate executable
  4494 code for ML and Haskell (including Isabelle classes).  A short usage
  4495 sketch:
  4496 
  4497     internal compilation:
  4498         export_code <list of constants (term syntax)> in SML
  4499     writing SML code to a file:
  4500         export_code <list of constants (term syntax)> in SML <filename>
  4501     writing OCaml code to a file:
  4502         export_code <list of constants (term syntax)> in OCaml <filename>
  4503     writing Haskell code to a bunch of files:
  4504         export_code <list of constants (term syntax)> in Haskell <filename>
  4505 
  4506     evaluating closed propositions to True/False using code generation:
  4507         method ``eval''
  4508 
  4509 Reasonable default setup of framework in HOL.
  4510 
  4511 Theorem attributs for selecting and transforming function equations theorems:
  4512 
  4513     [code fun]:        select a theorem as function equation for a specific constant
  4514     [code fun del]:    deselect a theorem as function equation for a specific constant
  4515     [code inline]:     select an equation theorem for unfolding (inlining) in place
  4516     [code inline del]: deselect an equation theorem for unfolding (inlining) in place
  4517 
  4518 User-defined serializations (target in {SML, OCaml, Haskell}):
  4519 
  4520     code_const <and-list of constants (term syntax)>
  4521       {(target) <and-list of const target syntax>}+
  4522 
  4523     code_type <and-list of type constructors>
  4524       {(target) <and-list of type target syntax>}+
  4525 
  4526     code_instance <and-list of instances>
  4527       {(target)}+
  4528         where instance ::= <type constructor> :: <class>
  4529 
  4530     code_class <and_list of classes>
  4531       {(target) <and-list of class target syntax>}+
  4532         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
  4533 
  4534 code_instance and code_class only are effective to target Haskell.
  4535 
  4536 For example usage see src/HOL/ex/Codegenerator.thy and
  4537 src/HOL/ex/Codegenerator_Pretty.thy.  A separate tutorial on code
  4538 generation from Isabelle/HOL theories is available via "isatool doc
  4539 codegen".
  4540 
  4541 * Code generator: consts in 'consts_code' Isar commands are now
  4542 referred to by usual term syntax (including optional type
  4543 annotations).
  4544 
  4545 * Command 'no_translations' removes translation rules from theory
  4546 syntax.
  4547 
  4548 * Overloaded definitions are now actually checked for acyclic
  4549 dependencies.  The overloading scheme is slightly more general than
  4550 that of Haskell98, although Isabelle does not demand an exact
  4551 correspondence to type class and instance declarations.
  4552 INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more
  4553 exotic versions of overloading -- at the discretion of the user!
  4554 
  4555 Polymorphic constants are represented via type arguments, i.e. the
  4556 instantiation that matches an instance against the most general
  4557 declaration given in the signature.  For example, with the declaration
  4558 c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented
  4559 as c(nat).  Overloading is essentially simultaneous structural
  4560 recursion over such type arguments.  Incomplete specification patterns
  4561 impose global constraints on all occurrences, e.g. c('a * 'a) on the
  4562 LHS means that more general c('a * 'b) will be disallowed on any RHS.
  4563 Command 'print_theory' outputs the normalized system of recursive
  4564 equations, see section "definitions".
  4565 
  4566 * Configuration options are maintained within the theory or proof
  4567 context (with name and type bool/int/string), providing a very simple
  4568 interface to a poor-man's version of general context data.  Tools may
  4569 declare options in ML (e.g. using Attrib.config_int) and then refer to
  4570 these values using Config.get etc.  Users may change options via an
  4571 associated attribute of the same name.  This form of context
  4572 declaration works particularly well with commands 'declare' or
  4573 'using', for example ``declare [[foo = 42]]''.  Thus it has become
  4574 very easy to avoid global references, which would not observe Isar
  4575 toplevel undo/redo and fail to work with multithreading.
  4576 
  4577 Various global ML references of Pure and HOL have been turned into
  4578 configuration options:
  4579 
  4580   Unify.search_bound		unify_search_bound
  4581   Unify.trace_bound		unify_trace_bound
  4582   Unify.trace_simp		unify_trace_simp
  4583   Unify.trace_types		unify_trace_types
  4584   Simplifier.simp_depth_limit	simp_depth_limit
  4585   Blast.depth_limit		blast_depth_limit
  4586   DatatypeProp.dtK		datatype_distinctness_limit
  4587   fast_arith_neq_limit  	fast_arith_neq_limit
  4588   fast_arith_split_limit	fast_arith_split_limit
  4589 
  4590 * Named collections of theorems may be easily installed as context
  4591 data using the functor NamedThmsFun (see also
  4592 src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
  4593 attributes; there is also a toplevel print command.  This facility is
  4594 just a common case of general context data, which is the preferred way
  4595 for anything more complex than just a list of facts in canonical
  4596 order.
  4597 
  4598 * Isar: command 'declaration' augments a local theory by generic
  4599 declaration functions written in ML.  This enables arbitrary content
  4600 being added to the context, depending on a morphism that tells the
  4601 difference of the original declaration context wrt. the application
  4602 context encountered later on.
  4603 
  4604 * Isar: proper interfaces for simplification procedures.  Command
  4605 'simproc_setup' declares named simprocs (with match patterns, and body
  4606 text in ML).  Attribute "simproc" adds/deletes simprocs in the current
  4607 context.  ML antiquotation @{simproc name} retrieves named simprocs.
  4608 
  4609 * Isar: an extra pair of brackets around attribute declarations
  4610 abbreviates a theorem reference involving an internal dummy fact,
  4611 which will be ignored later --- only the effect of the attribute on
  4612 the background context will persist.  This form of in-place
  4613 declarations is particularly useful with commands like 'declare' and
  4614 'using', for example ``have A using [[simproc a]] by simp''.
  4615 
  4616 * Isar: method "assumption" (and implicit closing of subproofs) now
  4617 takes simple non-atomic goal assumptions into account: after applying
  4618 an assumption as a rule the resulting subgoals are solved by atomic
  4619 assumption steps.  This is particularly useful to finish 'obtain'
  4620 goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",
  4621 without referring to the original premise "!!x. P x ==> thesis" in the
  4622 Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is
  4623 more permissive.
  4624 
  4625 * Isar: implicit use of prems from the Isar proof context is
  4626 considered a legacy feature.  Common applications like ``have A .''
  4627 may be replaced by ``have A by fact'' or ``note `A`''.  In general,
  4628 referencing facts explicitly here improves readability and
  4629 maintainability of proof texts.
  4630 
  4631 * Isar: improper proof element 'guess' is like 'obtain', but derives
  4632 the obtained context from the course of reasoning!  For example:
  4633 
  4634   assume "EX x y. A x & B y"   -- "any previous fact"
  4635   then guess x and y by clarify
  4636 
  4637 This technique is potentially adventurous, depending on the facts and
  4638 proof tools being involved here.
  4639 
  4640 * Isar: known facts from the proof context may be specified as literal
  4641 propositions, using ASCII back-quote syntax.  This works wherever
  4642 named facts used to be allowed so far, in proof commands, proof
  4643 methods, attributes etc.  Literal facts are retrieved from the context
  4644 according to unification of type and term parameters.  For example,
  4645 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
  4646 theorems in the current context, then these are valid literal facts:
  4647 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
  4648 
  4649 There is also a proof method "fact" which does the same composition
  4650 for explicit goal states, e.g. the following proof texts coincide with
  4651 certain special cases of literal facts:
  4652 
  4653   have "A" by fact                 ==  note `A`
  4654   have "A ==> B" by fact           ==  note `A ==> B`
  4655   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
  4656   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
  4657 
  4658 * Isar: ":" (colon) is no longer a symbolic identifier character in
  4659 outer syntax.  Thus symbolic identifiers may be used without
  4660 additional white space in declarations like this: ``assume *: A''.
  4661 
  4662 * Isar: 'print_facts' prints all local facts of the current context,
  4663 both named and unnamed ones.
  4664 
  4665 * Isar: 'def' now admits simultaneous definitions, e.g.:
  4666 
  4667   def x == "t" and y == "u"
  4668 
  4669 * Isar: added command 'unfolding', which is structurally similar to
  4670 'using', but affects both the goal state and facts by unfolding given
  4671 rewrite rules.  Thus many occurrences of the 'unfold' method or
  4672 'unfolded' attribute may be replaced by first-class proof text.
  4673 
  4674 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded',
  4675 and command 'unfolding' now all support object-level equalities
  4676 (potentially conditional).  The underlying notion of rewrite rule is
  4677 analogous to the 'rule_format' attribute, but *not* that of the
  4678 Simplifier (which is usually more generous).
  4679 
  4680 * Isar: the new attribute [rotated n] (default n = 1) rotates the
  4681 premises of a theorem by n. Useful in conjunction with drule.
  4682 
  4683 * Isar: the goal restriction operator [N] (default N = 1) evaluates a
  4684 method expression within a sandbox consisting of the first N
  4685 sub-goals, which need to exist.  For example, ``simp_all [3]''
  4686 simplifies the first three sub-goals, while (rule foo, simp_all)[]
  4687 simplifies all new goals that emerge from applying rule foo to the
  4688 originally first one.
  4689 
  4690 * Isar: schematic goals are no longer restricted to higher-order
  4691 patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as
  4692 expected.
  4693 
  4694 * Isar: the conclusion of a long theorem statement is now either
  4695 'shows' (a simultaneous conjunction, as before), or 'obtains'
  4696 (essentially a disjunction of cases with local parameters and
  4697 assumptions).  The latter allows to express general elimination rules
  4698 adequately; in this notation common elimination rules look like this:
  4699 
  4700   lemma exE:    -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis"
  4701     assumes "EX x. P x"
  4702     obtains x where "P x"
  4703 
  4704   lemma conjE:  -- "A & B ==> (A ==> B ==> thesis) ==> thesis"
  4705     assumes "A & B"
  4706     obtains A and B
  4707 
  4708   lemma disjE:  -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis"
  4709     assumes "A | B"
  4710     obtains
  4711       A
  4712     | B
  4713 
  4714 The subsequent classical rules even refer to the formal "thesis"
  4715 explicitly:
  4716 
  4717   lemma classical:     -- "(~ thesis ==> thesis) ==> thesis"
  4718     obtains "~ thesis"
  4719 
  4720   lemma Peirce's_Law:  -- "((thesis ==> something) ==> thesis) ==> thesis"
  4721     obtains "thesis ==> something"
  4722 
  4723 The actual proof of an 'obtains' statement is analogous to that of the
  4724 Isar proof element 'obtain', only that there may be several cases.
  4725 Optional case names may be specified in parentheses; these will be
  4726 available both in the present proof and as annotations in the
  4727 resulting rule, for later use with the 'cases' method (cf. attribute
  4728 case_names).
  4729 
  4730 * Isar: the assumptions of a long theorem statement are available as
  4731 "assms" fact in the proof context.  This is more appropriate than the
  4732 (historical) "prems", which refers to all assumptions of the current
  4733 context, including those from the target locale, proof body etc.
  4734 
  4735 * Isar: 'print_statement' prints theorems from the current theory or
  4736 proof context in long statement form, according to the syntax of a
  4737 top-level lemma.
  4738 
  4739 * Isar: 'obtain' takes an optional case name for the local context
  4740 introduction rule (default "that").
  4741 
  4742 * Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use
  4743 explicit (is "_ ==> ?foo") in the rare cases where this still happens
  4744 to occur.
  4745 
  4746 * Pure: syntax "CONST name" produces a fully internalized constant
  4747 according to the current context.  This is particularly useful for
  4748 syntax translations that should refer to internal constant
  4749 representations independently of name spaces.
  4750 
  4751 * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"
  4752 instead of "FOO ". This allows multiple binder declarations to coexist
  4753 in the same context.  INCOMPATIBILITY.
  4754 
  4755 * Isar/locales: 'notation' provides a robust interface to the 'syntax'
  4756 primitive that also works in a locale context (both for constants and
  4757 fixed variables). Type declaration and internal syntactic representation
  4758 of given constants retrieved from the context. Likewise, the
  4759 'no_notation' command allows to remove given syntax annotations from the
  4760 current context.
  4761 
  4762 * Isar/locales: new derived specification elements 'axiomatization',
  4763 'definition', 'abbreviation', which support type-inference, admit
  4764 object-level specifications (equality, equivalence).  See also the
  4765 isar-ref manual.  Examples:
  4766 
  4767   axiomatization
  4768     eq  (infix "===" 50) where
  4769     eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
  4770 
  4771   definition "f x y = x + y + 1"
  4772   definition g where "g x = f x x"
  4773 
  4774   abbreviation
  4775     neq  (infix "=!=" 50) where
  4776     "x =!= y == ~ (x === y)"
  4777 
  4778 These specifications may be also used in a locale context.  Then the
  4779 constants being introduced depend on certain fixed parameters, and the
  4780 constant name is qualified by the locale base name.  An internal
  4781 abbreviation takes care for convenient input and output, making the
  4782 parameters implicit and using the original short name.  See also
  4783 src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
  4784 entities from a monomorphic theory.
  4785 
  4786 Presently, abbreviations are only available 'in' a target locale, but
  4787 not inherited by general import expressions.  Also note that
  4788 'abbreviation' may be used as a type-safe replacement for 'syntax' +
  4789 'translations' in common applications.  The "no_abbrevs" print mode
  4790 prevents folding of abbreviations in term output.
  4791 
  4792 Concrete syntax is attached to specified constants in internal form,
  4793 independently of name spaces.  The parse tree representation is
  4794 slightly different -- use 'notation' instead of raw 'syntax', and
  4795 'translations' with explicit "CONST" markup to accommodate this.
  4796 
  4797 * Pure/Isar: unified syntax for new-style specification mechanisms
  4798 (e.g.  'definition', 'abbreviation', or 'inductive' in HOL) admits
  4799 full type inference and dummy patterns ("_").  For example:
  4800 
  4801   definition "K x _ = x"
  4802 
  4803   inductive conj for A B
  4804   where "A ==> B ==> conj A B"
  4805 
  4806 * Pure: command 'print_abbrevs' prints all constant abbreviations of
  4807 the current context.  Print mode "no_abbrevs" prevents inversion of
  4808 abbreviations on output.
  4809 
  4810 * Isar/locales: improved parameter handling: use of locales "var" and
  4811 "struct" no longer necessary; - parameter renamings are no longer
  4812 required to be injective.  For example, this allows to define
  4813 endomorphisms as locale endom = homom mult mult h.
  4814 
  4815 * Isar/locales: changed the way locales with predicates are defined.
  4816 Instead of accumulating the specification, the imported expression is
  4817 now an interpretation.  INCOMPATIBILITY: different normal form of
  4818 locale expressions.  In particular, in interpretations of locales with
  4819 predicates, goals repesenting already interpreted fragments are not
  4820 removed automatically.  Use methods `intro_locales' and
  4821 `unfold_locales'; see below.
  4822 
  4823 * Isar/locales: new methods `intro_locales' and `unfold_locales'
  4824 provide backward reasoning on locales predicates.  The methods are
  4825 aware of interpretations and discharge corresponding goals.
  4826 `intro_locales' is less aggressive then `unfold_locales' and does not
  4827 unfold predicates to assumptions.
  4828 
  4829 * Isar/locales: the order in which locale fragments are accumulated
  4830 has changed.  This enables to override declarations from fragments due
  4831 to interpretations -- for example, unwanted simp rules.
  4832 
  4833 * Isar/locales: interpretation in theories and proof contexts has been
  4834 extended.  One may now specify (and prove) equations, which are
  4835 unfolded in interpreted theorems.  This is useful for replacing
  4836 defined concepts (constants depending on locale parameters) by
  4837 concepts already existing in the target context.  Example:
  4838 
  4839   interpretation partial_order ["op <= :: [int, int] => bool"]
  4840     where "partial_order.less (op <=) (x::int) y = (x < y)"
  4841 
  4842 Typically, the constant `partial_order.less' is created by a
  4843 definition specification element in the context of locale
  4844 partial_order.
  4845 
  4846 * Method "induct": improved internal context management to support
  4847 local fixes and defines on-the-fly. Thus explicit meta-level
  4848 connectives !!  and ==> are rarely required anymore in inductive goals
  4849 (using object-logic connectives for this purpose has been long
  4850 obsolete anyway). Common proof patterns are explained in
  4851 src/HOL/Induct/Common_Patterns.thy, see also
  4852 src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic
  4853 examples.
  4854 
  4855 * Method "induct": improved handling of simultaneous goals. Instead of
  4856 introducing object-level conjunction, the statement is now split into
  4857 several conclusions, while the corresponding symbolic cases are nested
  4858 accordingly. INCOMPATIBILITY, proofs need to be structured explicitly,
  4859 see src/HOL/Induct/Common_Patterns.thy, for example.
  4860 
  4861 * Method "induct": mutual induction rules are now specified as a list
  4862 of rule sharing the same induction cases. HOL packages usually provide
  4863 foo_bar.inducts for mutually defined items foo and bar (e.g. inductive
  4864 predicates/sets or datatypes). INCOMPATIBILITY, users need to specify
  4865 mutual induction rules differently, i.e. like this:
  4866 
  4867   (induct rule: foo_bar.inducts)
  4868   (induct set: foo bar)
  4869   (induct pred: foo bar)
  4870   (induct type: foo bar)
  4871 
  4872 The ML function ProjectRule.projections turns old-style rules into the
  4873 new format.
  4874 
  4875 * Method "coinduct": dual of induction, see
  4876 src/HOL/Library/Coinductive_List.thy for various examples.
  4877 
  4878 * Method "cases", "induct", "coinduct": the ``(open)'' option is
  4879 considered a legacy feature.
  4880 
  4881 * Attribute "symmetric" produces result with standardized schematic
  4882 variables (index 0).  Potential INCOMPATIBILITY.
  4883 
  4884 * Simplifier: by default the simplifier trace only shows top level
  4885 rewrites now. That is, trace_simp_depth_limit is set to 1 by
  4886 default. Thus there is less danger of being flooded by the trace. The
  4887 trace indicates where parts have been suppressed.
  4888   
  4889 * Provers/classical: removed obsolete classical version of elim_format
  4890 attribute; classical elim/dest rules are now treated uniformly when
  4891 manipulating the claset.
  4892 
  4893 * Provers/classical: stricter checks to ensure that supplied intro,
  4894 dest and elim rules are well-formed; dest and elim rules must have at
  4895 least one premise.
  4896 
  4897 * Provers/classical: attributes dest/elim/intro take an optional
  4898 weight argument for the rule (just as the Pure versions).  Weights are
  4899 ignored by automated tools, but determine the search order of single
  4900 rule steps.
  4901 
  4902 * Syntax: input syntax now supports dummy variable binding "%_. b",
  4903 where the body does not mention the bound variable.  Note that dummy
  4904 patterns implicitly depend on their context of bounds, which makes
  4905 "{_. _}" match any set comprehension as expected.  Potential
  4906 INCOMPATIBILITY -- parse translations need to cope with syntactic
  4907 constant "_idtdummy" in the binding position.
  4908 
  4909 * Syntax: removed obsolete syntactic constant "_K" and its associated
  4910 parse translation.  INCOMPATIBILITY -- use dummy abstraction instead,
  4911 for example "A -> B" => "Pi A (%_. B)".
  4912 
  4913 * Pure: 'class_deps' command visualizes the subclass relation, using
  4914 the graph browser tool.
  4915 
  4916 * Pure: 'print_theory' now suppresses certain internal declarations by
  4917 default; use '!' option for full details.
  4918 
  4919 
  4920 *** HOL ***
  4921 
  4922 * Method "metis" proves goals by applying the Metis general-purpose
  4923 resolution prover (see also http://gilith.com/software/metis/).
  4924 Examples are in the directory MetisExamples.  WARNING: the
  4925 Isabelle/HOL-Metis integration does not yet work properly with
  4926 multi-threading.
  4927   
  4928 * Command 'sledgehammer' invokes external automatic theorem provers as
  4929 background processes.  It generates calls to the "metis" method if
  4930 successful. These can be pasted into the proof.  Users do not have to
  4931 wait for the automatic provers to return.  WARNING: does not really
  4932 work with multi-threading.
  4933 
  4934 * New "auto_quickcheck" feature tests outermost goal statements for
  4935 potential counter-examples.  Controlled by ML references
  4936 auto_quickcheck (default true) and auto_quickcheck_time_limit (default
  4937 5000 milliseconds).  Fails silently if statements is outside of
  4938 executable fragment, or any other codgenerator problem occurs.
  4939 
  4940 * New constant "undefined" with axiom "undefined x = undefined".
  4941 
  4942 * Added class "HOL.eq", allowing for code generation with polymorphic
  4943 equality.
  4944 
  4945 * Some renaming of class constants due to canonical name prefixing in
  4946 the new 'class' package:
  4947 
  4948     HOL.abs ~> HOL.abs_class.abs
  4949     HOL.divide ~> HOL.divide_class.divide
  4950     0 ~> HOL.zero_class.zero
  4951     1 ~> HOL.one_class.one
  4952     op + ~> HOL.plus_class.plus
  4953     op - ~> HOL.minus_class.minus
  4954     uminus ~> HOL.minus_class.uminus
  4955     op * ~> HOL.times_class.times
  4956     op < ~> HOL.ord_class.less
  4957     op <= > HOL.ord_class.less_eq
  4958     Nat.power ~> Power.power_class.power
  4959     Nat.size ~> Nat.size_class.size
  4960     Numeral.number_of ~> Numeral.number_class.number_of
  4961     FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf
  4962     FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup
  4963     Orderings.min ~> Orderings.ord_class.min
  4964     Orderings.max ~> Orderings.ord_class.max
  4965     Divides.op div ~> Divides.div_class.div
  4966     Divides.op mod ~> Divides.div_class.mod
  4967     Divides.op dvd ~> Divides.div_class.dvd
  4968 
  4969 INCOMPATIBILITY.  Adaptions may be required in the following cases:
  4970 
  4971 a) User-defined constants using any of the names "plus", "minus",
  4972 "times", "less" or "less_eq". The standard syntax translations for
  4973 "+", "-" and "*" may go wrong.  INCOMPATIBILITY: use more specific
  4974 names.
  4975 
  4976 b) Variables named "plus", "minus", "times", "less", "less_eq"
  4977 INCOMPATIBILITY: use more specific names.
  4978 
  4979 c) Permutative equations (e.g. "a + b = b + a")
  4980 Since the change of names also changes the order of terms, permutative
  4981 rewrite rules may get applied in a different order. Experience shows
  4982 that this is rarely the case (only two adaptions in the whole Isabelle
  4983 distribution).  INCOMPATIBILITY: rewrite proofs
  4984 
  4985 d) ML code directly refering to constant names
  4986 This in general only affects hand-written proof tactics, simprocs and
  4987 so on.  INCOMPATIBILITY: grep your sourcecode and replace names.
  4988 Consider using @{const_name} antiquotation.
  4989 
  4990 * New class "default" with associated constant "default".
  4991 
  4992 * Function "sgn" is now overloaded and available on int, real, complex
  4993 (and other numeric types), using class "sgn".  Two possible defs of
  4994 sgn are given as equational assumptions in the classes sgn_if and
  4995 sgn_div_norm; ordered_idom now also inherits from sgn_if.
  4996 INCOMPATIBILITY.
  4997 
  4998 * Locale "partial_order" now unified with class "order" (cf. theory
  4999 Orderings), added parameter "less".  INCOMPATIBILITY.
  5000 
  5001 * Renamings in classes "order" and "linorder": facts "refl", "trans" and
  5002 "cases" to "order_refl", "order_trans" and "linorder_cases", to avoid
  5003 clashes with HOL "refl" and "trans".  INCOMPATIBILITY.
  5004 
  5005 * Classes "order" and "linorder": potential INCOMPATIBILITY due to
  5006 changed order of proof goals in instance proofs.
  5007 
  5008 * The transitivity reasoner for partial and linear orders is set up
  5009 for classes "order" and "linorder".  Instances of the reasoner are available
  5010 in all contexts importing or interpreting the corresponding locales.
  5011 Method "order" invokes the reasoner separately; the reasoner
  5012 is also integrated with the Simplifier as a solver.  Diagnostic
  5013 command 'print_orders' shows the available instances of the reasoner
  5014 in the current context.
  5015 
  5016 * Localized monotonicity predicate in theory "Orderings"; integrated
  5017 lemmas max_of_mono and min_of_mono with this predicate.
  5018 INCOMPATIBILITY.
  5019 
  5020 * Formulation of theorem "dense" changed slightly due to integration
  5021 with new class dense_linear_order.
  5022 
  5023 * Uniform lattice theory development in HOL.
  5024 
  5025     constants "meet" and "join" now named "inf" and "sup"
  5026     constant "Meet" now named "Inf"
  5027 
  5028     classes "meet_semilorder" and "join_semilorder" now named
  5029       "lower_semilattice" and "upper_semilattice"
  5030     class "lorder" now named "lattice"
  5031     class "comp_lat" now named "complete_lattice"
  5032 
  5033     Instantiation of lattice classes allows explicit definitions
  5034     for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices).
  5035 
  5036   INCOMPATIBILITY.  Theorem renames:
  5037 
  5038     meet_left_le            ~> inf_le1
  5039     meet_right_le           ~> inf_le2
  5040     join_left_le            ~> sup_ge1
  5041     join_right_le           ~> sup_ge2
  5042     meet_join_le            ~> inf_sup_ord
  5043     le_meetI                ~> le_infI
  5044     join_leI                ~> le_supI
  5045     le_meet                 ~> le_inf_iff
  5046     le_join                 ~> ge_sup_conv
  5047     meet_idempotent         ~> inf_idem
  5048     join_idempotent         ~> sup_idem
  5049     meet_comm               ~> inf_commute
  5050     join_comm               ~> sup_commute
  5051     meet_leI1               ~> le_infI1
  5052     meet_leI2               ~> le_infI2
  5053     le_joinI1               ~> le_supI1
  5054     le_joinI2               ~> le_supI2
  5055     meet_assoc              ~> inf_assoc
  5056     join_assoc              ~> sup_assoc
  5057     meet_left_comm          ~> inf_left_commute
  5058     meet_left_idempotent    ~> inf_left_idem
  5059     join_left_comm          ~> sup_left_commute
  5060     join_left_idempotent    ~> sup_left_idem
  5061     meet_aci                ~> inf_aci
  5062     join_aci                ~> sup_aci
  5063     le_def_meet             ~> le_iff_inf
  5064     le_def_join             ~> le_iff_sup
  5065     join_absorp2            ~> sup_absorb2
  5066     join_absorp1            ~> sup_absorb1
  5067     meet_absorp1            ~> inf_absorb1
  5068     meet_absorp2            ~> inf_absorb2
  5069     meet_join_absorp        ~> inf_sup_absorb
  5070     join_meet_absorp        ~> sup_inf_absorb
  5071     distrib_join_le         ~> distrib_sup_le
  5072     distrib_meet_le         ~> distrib_inf_le
  5073 
  5074     add_meet_distrib_left   ~> add_inf_distrib_left
  5075     add_join_distrib_left   ~> add_sup_distrib_left
  5076     is_join_neg_meet        ~> is_join_neg_inf
  5077     is_meet_neg_join        ~> is_meet_neg_sup
  5078     add_meet_distrib_right  ~> add_inf_distrib_right
  5079     add_join_distrib_right  ~> add_sup_distrib_right
  5080     add_meet_join_distribs  ~> add_sup_inf_distribs
  5081     join_eq_neg_meet        ~> sup_eq_neg_inf
  5082     meet_eq_neg_join        ~> inf_eq_neg_sup
  5083     add_eq_meet_join        ~> add_eq_inf_sup
  5084     meet_0_imp_0            ~> inf_0_imp_0
  5085     join_0_imp_0            ~> sup_0_imp_0
  5086     meet_0_eq_0             ~> inf_0_eq_0
  5087     join_0_eq_0             ~> sup_0_eq_0
  5088     neg_meet_eq_join        ~> neg_inf_eq_sup
  5089     neg_join_eq_meet        ~> neg_sup_eq_inf
  5090     join_eq_if              ~> sup_eq_if
  5091 
  5092     mono_meet               ~> mono_inf
  5093     mono_join               ~> mono_sup
  5094     meet_bool_eq            ~> inf_bool_eq
  5095     join_bool_eq            ~> sup_bool_eq
  5096     meet_fun_eq             ~> inf_fun_eq
  5097     join_fun_eq             ~> sup_fun_eq
  5098     meet_set_eq             ~> inf_set_eq
  5099     join_set_eq             ~> sup_set_eq
  5100     meet1_iff               ~> inf1_iff
  5101     meet2_iff               ~> inf2_iff
  5102     meet1I                  ~> inf1I
  5103     meet2I                  ~> inf2I
  5104     meet1D1                 ~> inf1D1
  5105     meet2D1                 ~> inf2D1
  5106     meet1D2                 ~> inf1D2
  5107     meet2D2                 ~> inf2D2
  5108     meet1E                  ~> inf1E
  5109     meet2E                  ~> inf2E
  5110     join1_iff               ~> sup1_iff
  5111     join2_iff               ~> sup2_iff
  5112     join1I1                 ~> sup1I1
  5113     join2I1                 ~> sup2I1
  5114     join1I1                 ~> sup1I1
  5115     join2I2                 ~> sup1I2
  5116     join1CI                 ~> sup1CI
  5117     join2CI                 ~> sup2CI
  5118     join1E                  ~> sup1E
  5119     join2E                  ~> sup2E
  5120 
  5121     is_meet_Meet            ~> is_meet_Inf
  5122     Meet_bool_def           ~> Inf_bool_def
  5123     Meet_fun_def            ~> Inf_fun_def
  5124     Meet_greatest           ~> Inf_greatest
  5125     Meet_lower              ~> Inf_lower
  5126     Meet_set_def            ~> Inf_set_def
  5127 
  5128     Sup_def                 ~> Sup_Inf
  5129     Sup_bool_eq             ~> Sup_bool_def
  5130     Sup_fun_eq              ~> Sup_fun_def
  5131     Sup_set_eq              ~> Sup_set_def
  5132 
  5133     listsp_meetI            ~> listsp_infI
  5134     listsp_meet_eq          ~> listsp_inf_eq
  5135 
  5136     meet_min                ~> inf_min
  5137     join_max                ~> sup_max
  5138 
  5139 * Added syntactic class "size"; overloaded constant "size" now has
  5140 type "'a::size ==> bool"
  5141 
  5142 * Internal reorganisation of `size' of datatypes: size theorems
  5143 "foo.size" are no longer subsumed by "foo.simps" (but are still
  5144 simplification rules by default!); theorems "prod.size" now named
  5145 "*.size".
  5146 
  5147 * Class "div" now inherits from class "times" rather than "type".
  5148 INCOMPATIBILITY.
  5149 
  5150 * HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice,
  5151 Linorder etc.  have disappeared; operations defined in terms of
  5152 fold_set now are named Inf_fin, Sup_fin.  INCOMPATIBILITY.
  5153 
  5154 * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
  5155 
  5156 * HOL-Word: New extensive library and type for generic, fixed size
  5157 machine words, with arithemtic, bit-wise, shifting and rotating
  5158 operations, reflection into int, nat, and bool lists, automation for
  5159 linear arithmetic (by automatic reflection into nat or int), including
  5160 lemmas on overflow and monotonicity.  Instantiated to all appropriate
  5161 arithmetic type classes, supporting automatic simplification of
  5162 numerals on all operations.
  5163 
  5164 * Library/Boolean_Algebra: locales for abstract boolean algebras.
  5165 
  5166 * Library/Numeral_Type: numbers as types, e.g. TYPE(32).
  5167 
  5168 * Code generator library theories:
  5169   - Code_Integer represents HOL integers by big integer literals in target
  5170     languages.
  5171   - Code_Char represents HOL characters by character literals in target
  5172     languages.
  5173   - Code_Char_chr like Code_Char, but also offers treatment of character
  5174     codes; includes Code_Integer.
  5175   - Executable_Set allows to generate code for finite sets using lists.
  5176   - Executable_Rat implements rational numbers as triples (sign, enumerator,
  5177     denominator).
  5178   - Executable_Real implements a subset of real numbers, namly those
  5179     representable by rational numbers.
  5180   - Efficient_Nat implements natural numbers by integers, which in general will
  5181     result in higher efficency; pattern matching with 0/Suc is eliminated;
  5182     includes Code_Integer.
  5183   - Code_Index provides an additional datatype index which is mapped to
  5184     target-language built-in integers.
  5185   - Code_Message provides an additional datatype message_string which is isomorphic to
  5186     strings; messages are mapped to target-language strings.
  5187 
  5188 * New package for inductive predicates
  5189 
  5190   An n-ary predicate p with m parameters z_1, ..., z_m can now be defined via
  5191 
  5192     inductive
  5193       p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  5194       for z_1 :: U_1 and ... and z_n :: U_m
  5195     where
  5196       rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
  5197     | ...
  5198 
  5199   with full support for type-inference, rather than
  5200 
  5201     consts s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  5202 
  5203     abbreviation p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  5204     where "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
  5205 
  5206     inductive "s z_1 ... z_m"
  5207     intros
  5208       rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
  5209       ...
  5210 
  5211   For backward compatibility, there is a wrapper allowing inductive
  5212   sets to be defined with the new package via
  5213 
  5214     inductive_set
  5215       s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  5216       for z_1 :: U_1 and ... and z_n :: U_m
  5217     where
  5218       rule_1: "... ==> (t_1_1, ..., t_1_n) : s z_1 ... z_m"
  5219     | ...
  5220 
  5221   or
  5222 
  5223     inductive_set
  5224       s :: "U_1 => ... => U_m => (T_1 * ... * T_n) set"
  5225       and p :: "U_1 => ... => U_m => T_1 => ... => T_n => bool"
  5226       for z_1 :: U_1 and ... and z_n :: U_m
  5227     where
  5228       "p z_1 ... z_m x_1 ... x_n == (x_1, ..., x_n) : s z_1 ... z_m"
  5229     | rule_1: "... ==> p z_1 ... z_m t_1_1 ... t_1_n"
  5230     | ...
  5231 
  5232   if the additional syntax "p ..." is required.
  5233 
  5234   Numerous examples can be found in the subdirectories src/HOL/Auth,
  5235   src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava.
  5236 
  5237   INCOMPATIBILITIES:
  5238 
  5239   - Since declaration and definition of inductive sets or predicates
  5240     is no longer separated, abbreviations involving the newly
  5241     introduced sets or predicates must be specified together with the
  5242     introduction rules after the 'where' keyword (see above), rather
  5243     than before the actual inductive definition.
  5244 
  5245   - The variables in induction and elimination rules are now
  5246     quantified in the order of their occurrence in the introduction
  5247     rules, rather than in alphabetical order. Since this may break
  5248     some proofs, these proofs either have to be repaired, e.g. by
  5249     reordering the variables a_i_1 ... a_i_{k_i} in Isar 'case'
  5250     statements of the form
  5251 
  5252       case (rule_i a_i_1 ... a_i_{k_i})
  5253 
  5254     or the old order of quantification has to be restored by explicitly adding
  5255     meta-level quantifiers in the introduction rules, i.e.
  5256 
  5257       | rule_i: "!!a_i_1 ... a_i_{k_i}. ... ==> p z_1 ... z_m t_i_1 ... t_i_n"
  5258 
  5259   - The format of the elimination rules is now
  5260 
  5261       p z_1 ... z_m x_1 ... x_n ==>
  5262         (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
  5263         ==> ... ==> P
  5264 
  5265     for predicates and
  5266 
  5267       (x_1, ..., x_n) : s z_1 ... z_m ==>
  5268         (!!a_1_1 ... a_1_{k_1}. x_1 = t_1_1 ==> ... ==> x_n = t_1_n ==> ... ==> P)
  5269         ==> ... ==> P
  5270 
  5271     for sets rather than
  5272 
  5273       x : s z_1 ... z_m ==>
  5274         (!!a_1_1 ... a_1_{k_1}. x = (t_1_1, ..., t_1_n) ==> ... ==> P)
  5275         ==> ... ==> P
  5276 
  5277     This may require terms in goals to be expanded to n-tuples
  5278     (e.g. using case_tac or simplification with the split_paired_all
  5279     rule) before the above elimination rule is applicable.
  5280 
  5281   - The elimination or case analysis rules for (mutually) inductive
  5282     sets or predicates are now called "p_1.cases" ... "p_k.cases". The
  5283     list of rules "p_1_..._p_k.elims" is no longer available.
  5284 
  5285 * New package "function"/"fun" for general recursive functions,
  5286 supporting mutual and nested recursion, definitions in local contexts,
  5287 more general pattern matching and partiality. See HOL/ex/Fundefs.thy
  5288 for small examples, and the separate tutorial on the function
  5289 package. The old recdef "package" is still available as before, but
  5290 users are encouraged to use the new package.
  5291 
  5292 * Method "lexicographic_order" automatically synthesizes termination
  5293 relations as lexicographic combinations of size measures. 
  5294 
  5295 * Case-expressions allow arbitrary constructor-patterns (including
  5296 "_") and take their order into account, like in functional
  5297 programming.  Internally, this is translated into nested
  5298 case-expressions; missing cases are added and mapped to the predefined
  5299 constant "undefined". In complicated cases printing may no longer show
  5300 the original input but the internal form. Lambda-abstractions allow
  5301 the same form of pattern matching: "% pat1 => e1 | ..." is an
  5302 abbreviation for "%x. case x of pat1 => e1 | ..." where x is a new
  5303 variable.
  5304 
  5305 * IntDef: The constant "int :: nat => int" has been removed; now "int"
  5306 is an abbreviation for "of_nat :: nat => int". The simplification
  5307 rules for "of_nat" have been changed to work like "int" did
  5308 previously.  Potential INCOMPATIBILITY:
  5309   - "of_nat (Suc m)" simplifies to "1 + of_nat m" instead of "of_nat m + 1"
  5310   - of_nat_diff and of_nat_mult are no longer default simp rules
  5311 
  5312 * Method "algebra" solves polynomial equations over (semi)rings using
  5313 Groebner bases. The (semi)ring structure is defined by locales and the
  5314 tool setup depends on that generic context. Installing the method for
  5315 a specific type involves instantiating the locale and possibly adding
  5316 declarations for computation on the coefficients.  The method is
  5317 already instantiated for natural numbers and for the axiomatic class
  5318 of idoms with numerals.  See also the paper by Chaieb and Wenzel at
  5319 CALCULEMUS 2007 for the general principles underlying this
  5320 architecture of context-aware proof-tools.
  5321 
  5322 * Method "ferrack" implements quantifier elimination over
  5323 special-purpose dense linear orders using locales (analogous to
  5324 "algebra"). The method is already installed for class
  5325 {ordered_field,recpower,number_ring} which subsumes real, hyperreal,
  5326 rat, etc.
  5327 
  5328 * Former constant "List.op @" now named "List.append".  Use ML
  5329 antiquotations @{const_name List.append} or @{term " ... @ ... "} to
  5330 circumvent possible incompatibilities when working on ML level.
  5331 
  5332 * primrec: missing cases mapped to "undefined" instead of "arbitrary".
  5333 
  5334 * New function listsum :: 'a list => 'a for arbitrary monoids.
  5335 Special syntax: "SUM x <- xs. f x" (and latex variants)
  5336 
  5337 * New syntax for Haskell-like list comprehension (input only), eg.
  5338 [(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy.
  5339 
  5340 * The special syntax for function "filter" has changed from [x :
  5341 xs. P] to [x <- xs. P] to avoid an ambiguity caused by list
  5342 comprehension syntax, and for uniformity.  INCOMPATIBILITY.
  5343 
  5344 * [a..b] is now defined for arbitrary linear orders.  It used to be
  5345 defined on nat only, as an abbreviation for [a..<Suc b]
  5346 INCOMPATIBILITY.
  5347 
  5348 * Renamed lemma "set_take_whileD"  to "set_takeWhileD".
  5349 
  5350 * New functions "sorted" and "sort" in src/HOL/List.thy.
  5351 
  5352 * New lemma collection field_simps (an extension of ring_simps) for
  5353 manipulating (in)equations involving division. Multiplies with all
  5354 denominators that can be proved to be non-zero (in equations) or
  5355 positive/negative (in inequations).
  5356 
  5357 * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib
  5358 have been improved and renamed to ring_simps, group_simps and
  5359 ring_distribs.  Removed lemmas field_xyz in theory Ring_and_Field
  5360 because they were subsumed by lemmas xyz.  INCOMPATIBILITY.
  5361 
  5362 * Theory Library/Commutative_Ring: switched from recdef to function
  5363 package; constants add, mul, pow now curried.  Infix syntax for
  5364 algebraic operations.
  5365 
  5366 * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
  5367 INCOMPATIBILITY.
  5368 
  5369 * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj.
  5370 INCOMPATIBILITY.
  5371 
  5372 * HOL/records: generalised field-update to take a function on the
  5373 field rather than the new value: r(|A := x|) is translated to A_update
  5374 (K x) r The K-combinator that is internally used is called K_record.
  5375 INCOMPATIBILITY: Usage of the plain update functions has to be
  5376 adapted.
  5377  
  5378 * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0
  5379 * x = 0, which are required for a semiring.  Richer structures do not
  5380 inherit from semiring_0 anymore, because this property is a theorem
  5381 there, not an axiom.  INCOMPATIBILITY: In instances of semiring_0,
  5382 there is more to prove, but this is mostly trivial.
  5383 
  5384 * Class "recpower" is generalized to arbitrary monoids, not just
  5385 commutative semirings.  INCOMPATIBILITY: may need to incorporate
  5386 commutativity or semiring properties additionally.
  5387 
  5388 * Constant "List.list_all2" in List.thy now uses authentic syntax.
  5389 INCOMPATIBILITY: translations containing list_all2 may go wrong,
  5390 better use 'abbreviation'.
  5391 
  5392 * Renamed constant "List.op mem" to "List.member".  INCOMPATIBILITY.
  5393 
  5394 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has
  5395 been abandoned in favour of plain 'int'.  INCOMPATIBILITY --
  5396 significant changes for setting up numeral syntax for types:
  5397   - New constants Numeral.pred and Numeral.succ instead
  5398       of former Numeral.bin_pred and Numeral.bin_succ.
  5399   - Use integer operations instead of bin_add, bin_mult and so on.
  5400   - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
  5401   - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
  5402 
  5403 See src/HOL/Integ/IntArith.thy for an example setup.
  5404 
  5405 * Command 'normal_form' computes the normal form of a term that may
  5406 contain free variables.  For example ``normal_form "rev [a, b, c]"''
  5407 produces ``[b, c, a]'' (without proof).  This command is suitable for
  5408 heavy-duty computations because the functions are compiled to ML
  5409 first.  Correspondingly, a method "normalization" is provided.  See
  5410 further src/HOL/ex/NormalForm.thy and src/Tools/nbe.ML.
  5411 
  5412 * Alternative iff syntax "A <-> B" for equality on bool (with priority
  5413 25 like -->); output depends on the "iff" print_mode, the default is
  5414 "A = B" (with priority 50).
  5415 
  5416 * Relations less (<) and less_eq (<=) are also available on type bool.
  5417 Modified syntax to disallow nesting without explicit parentheses,
  5418 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".  Potential
  5419 INCOMPATIBILITY.
  5420 
  5421 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
  5422 
  5423 * Relation composition operator "op O" now has precedence 75 and binds
  5424 stronger than union and intersection. INCOMPATIBILITY.
  5425 
  5426 * The old set interval syntax "{m..n(}" (and relatives) has been
  5427 removed.  Use "{m..<n}" (and relatives) instead.
  5428 
  5429 * In the context of the assumption "~(s = t)" the Simplifier rewrites
  5430 "t = s" to False (by simproc "neq").  INCOMPATIBILITY, consider using
  5431 ``declare [[simproc del: neq]]''.
  5432 
  5433 * Simplifier: "m dvd n" where m and n are numbers is evaluated to
  5434 True/False.
  5435 
  5436 * Theorem Cons_eq_map_conv no longer declared as "simp".
  5437 
  5438 * Theorem setsum_mult renamed to setsum_right_distrib.
  5439 
  5440 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
  5441 ``rule'' method.
  5442 
  5443 * Reimplemented methods "sat" and "satx", with several improvements:
  5444 goals no longer need to be stated as "<prems> ==> False", equivalences
  5445 (i.e. "=" on type bool) are handled, variable names of the form
  5446 "lit_<n>" are no longer reserved, significant speedup.
  5447 
  5448 * Methods "sat" and "satx" can now replay MiniSat proof traces.
  5449 zChaff is still supported as well.
  5450 
  5451 * 'inductive' and 'datatype': provide projections of mutual rules,
  5452 bundled as foo_bar.inducts;
  5453 
  5454 * Library: moved theories Parity, GCD, Binomial, Infinite_Set to
  5455 Library.
  5456 
  5457 * Library: moved theory Accessible_Part to main HOL.
  5458 
  5459 * Library: added theory Coinductive_List of potentially infinite lists
  5460 as greatest fixed-point.
  5461 
  5462 * Library: added theory AssocList which implements (finite) maps as
  5463 association lists.
  5464 
  5465 * Method "evaluation" solves goals (i.e. a boolean expression)
  5466 efficiently by compiling it to ML.  The goal is "proved" (via an
  5467 oracle) if it evaluates to True.
  5468 
  5469 * Linear arithmetic now splits certain operators (e.g. min, max, abs)
  5470 also when invoked by the simplifier.  This results in the Simplifier
  5471 being more powerful on arithmetic goals.  INCOMPATIBILITY.
  5472 Configuration option fast_arith_split_limit=0 recovers the old
  5473 behavior.
  5474 
  5475 * Support for hex (0x20) and binary (0b1001) numerals.
  5476 
  5477 * New method: reify eqs (t), where eqs are equations for an
  5478 interpretation I :: 'a list => 'b => 'c and t::'c is an optional
  5479 parameter, computes a term s::'b and a list xs::'a list and proves the
  5480 theorem I xs s = t. This is also known as reification or quoting. The
  5481 resulting theorem is applied to the subgoal to substitute t with I xs
  5482 s.  If t is omitted, the subgoal itself is reified.
  5483 
  5484 * New method: reflection corr_thm eqs (t). The parameters eqs and (t)
  5485 are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
  5486 where f is supposed to be a computable function (in the sense of code
  5487 generattion). The method uses reify to compute s and xs as above then
  5488 applies corr_thm and uses normalization by evaluation to "prove" f s =
  5489 r and finally gets the theorem t = r, which is again applied to the
  5490 subgoal. An Example is available in src/HOL/ex/ReflectionEx.thy.
  5491 
  5492 * Reflection: Automatic reification now handels binding, an example is
  5493 available in src/HOL/ex/ReflectionEx.thy
  5494 
  5495 * HOL-Statespace: ``State Spaces: The Locale Way'' introduces a
  5496 command 'statespace' that is similar to 'record', but introduces an
  5497 abstract specification based on the locale infrastructure instead of
  5498 HOL types.  This leads to extra flexibility in composing state spaces,
  5499 in particular multiple inheritance and renaming of components.
  5500 
  5501 
  5502 *** HOL-Complex ***
  5503 
  5504 * Hyperreal: Functions root and sqrt are now defined on negative real
  5505 inputs so that root n (- x) = - root n x and sqrt (- x) = - sqrt x.
  5506 Nonnegativity side conditions have been removed from many lemmas, so
  5507 that more subgoals may now be solved by simplification; potential
  5508 INCOMPATIBILITY.
  5509 
  5510 * Real: new type classes formalize real normed vector spaces and
  5511 algebras, using new overloaded constants scaleR :: real => 'a => 'a
  5512 and norm :: 'a => real.
  5513 
  5514 * Real: constant of_real :: real => 'a::real_algebra_1 injects from
  5515 reals into other types. The overloaded constant Reals :: 'a set is now
  5516 defined as range of_real; potential INCOMPATIBILITY.
  5517 
  5518 * Real: proper support for ML code generation, including 'quickcheck'.
  5519 Reals are implemented as arbitrary precision rationals.
  5520 
  5521 * Hyperreal: Several constants that previously worked only for the
  5522 reals have been generalized, so they now work over arbitrary vector
  5523 spaces. Type annotations may need to be added in some cases; potential
  5524 INCOMPATIBILITY.
  5525 
  5526   Infinitesimal  :: ('a::real_normed_vector) star set
  5527   HFinite        :: ('a::real_normed_vector) star set
  5528   HInfinite      :: ('a::real_normed_vector) star set
  5529   approx         :: ('a::real_normed_vector) star => 'a star => bool
  5530   monad          :: ('a::real_normed_vector) star => 'a star set
  5531   galaxy         :: ('a::real_normed_vector) star => 'a star set
  5532   (NS)LIMSEQ     :: [nat => 'a::real_normed_vector, 'a] => bool
  5533   (NS)convergent :: (nat => 'a::real_normed_vector) => bool
  5534   (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
  5535   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
  5536   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
  5537   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
  5538   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
  5539   sgn            :: 'a::real_normed_vector => 'a
  5540   exp            :: 'a::{recpower,real_normed_field,banach} => 'a
  5541 
  5542 * Complex: Some complex-specific constants are now abbreviations for
  5543 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
  5544 hnorm.  Other constants have been entirely removed in favor of the
  5545 polymorphic versions (INCOMPATIBILITY):
  5546 
  5547   approx        <-- capprox
  5548   HFinite       <-- CFinite
  5549   HInfinite     <-- CInfinite
  5550   Infinitesimal <-- CInfinitesimal
  5551   monad         <-- cmonad
  5552   galaxy        <-- cgalaxy
  5553   (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
  5554   is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
  5555   (ns)deriv     <-- (ns)cderiv
  5556 
  5557 
  5558 *** HOL-Algebra ***
  5559 
  5560 * Formalisation of ideals and the quotient construction over rings.
  5561 
  5562 * Order and lattice theory no longer based on records.
  5563 INCOMPATIBILITY.
  5564 
  5565 * Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
  5566 greatest_closed.  INCOMPATIBILITY.
  5567 
  5568 * Method algebra is now set up via an attribute.  For examples see
  5569 Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
  5570 of algebraic structures.
  5571 
  5572 * Renamed theory CRing to Ring.
  5573 
  5574 
  5575 *** HOL-Nominal ***
  5576 
  5577 * Substantial, yet incomplete support for nominal datatypes (binding
  5578 structures) based on HOL-Nominal logic.  See src/HOL/Nominal and
  5579 src/HOL/Nominal/Examples.  Prospective users should consult
  5580 http://isabelle.in.tum.de/nominal/
  5581 
  5582 
  5583 *** ML ***
  5584 
  5585 * ML basics: just one true type int, which coincides with IntInf.int
  5586 (even on SML/NJ).
  5587 
  5588 * ML within Isar: antiquotations allow to embed statically-checked
  5589 formal entities in the source, referring to the context available at
  5590 compile-time.  For example:
  5591 
  5592 ML {* @{sort "{zero,one}"} *}
  5593 ML {* @{typ "'a => 'b"} *}
  5594 ML {* @{term "%x. x"} *}
  5595 ML {* @{prop "x == y"} *}
  5596 ML {* @{ctyp "'a => 'b"} *}
  5597 ML {* @{cterm "%x. x"} *}
  5598 ML {* @{cprop "x == y"} *}
  5599 ML {* @{thm asm_rl} *}
  5600 ML {* @{thms asm_rl} *}
  5601 ML {* @{type_name c} *}
  5602 ML {* @{type_syntax c} *}
  5603 ML {* @{const_name c} *}
  5604 ML {* @{const_syntax c} *}
  5605 ML {* @{context} *}
  5606 ML {* @{theory} *}
  5607 ML {* @{theory Pure} *}
  5608 ML {* @{theory_ref} *}
  5609 ML {* @{theory_ref Pure} *}
  5610 ML {* @{simpset} *}
  5611 ML {* @{claset} *}
  5612 ML {* @{clasimpset} *}
  5613 
  5614 The same works for sources being ``used'' within an Isar context.
  5615 
  5616 * ML in Isar: improved error reporting; extra verbosity with
  5617 ML_Context.trace enabled.
  5618 
  5619 * Pure/General/table.ML: the join operations now works via exceptions
  5620 DUP/SAME instead of type option. This is simpler in simple cases, and
  5621 admits slightly more efficient complex applications.
  5622 
  5623 * Pure: 'advanced' translation functions (parse_translation etc.) now
  5624 use Context.generic instead of just theory.
  5625 
  5626 * Pure: datatype Context.generic joins theory/Proof.context and
  5627 provides some facilities for code that works in either kind of
  5628 context, notably GenericDataFun for uniform theory and proof data.
  5629 
  5630 * Pure: simplified internal attribute type, which is now always
  5631 Context.generic * thm -> Context.generic * thm. Global (theory) vs.
  5632 local (Proof.context) attributes have been discontinued, while
  5633 minimizing code duplication. Thm.rule_attribute and
  5634 Thm.declaration_attribute build canonical attributes; see also structure
  5635 Context for further operations on Context.generic, notably
  5636 GenericDataFun. INCOMPATIBILITY, need to adapt attribute type
  5637 declarations and definitions.
  5638 
  5639 * Context data interfaces (Theory/Proof/GenericDataFun): removed
  5640 name/print, uninitialized data defaults to ad-hoc copy of empty value,
  5641 init only required for impure data. INCOMPATIBILITY: empty really need
  5642 to be empty (no dependencies on theory content!)
  5643 
  5644 * Pure/kernel: consts certification ignores sort constraints given in
  5645 signature declarations. (This information is not relevant to the
  5646 logic, but only for type inference.) SIGNIFICANT INTERNAL CHANGE,
  5647 potential INCOMPATIBILITY.
  5648 
  5649 * Pure: axiomatic type classes are now purely definitional, with
  5650 explicit proofs of class axioms and super class relations performed
  5651 internally. See Pure/axclass.ML for the main internal interfaces --
  5652 notably AxClass.define_class supercedes AxClass.add_axclass, and
  5653 AxClass.axiomatize_class/classrel/arity supersede
  5654 Sign.add_classes/classrel/arities.
  5655 
  5656 * Pure/Isar: Args/Attrib parsers operate on Context.generic --
  5657 global/local versions on theory vs. Proof.context have been
  5658 discontinued; Attrib.syntax and Method.syntax have been adapted
  5659 accordingly.  INCOMPATIBILITY, need to adapt parser expressions for
  5660 attributes, methods, etc.
  5661 
  5662 * Pure: several functions of signature "... -> theory -> theory * ..."
  5663 have been reoriented to "... -> theory -> ... * theory" in order to
  5664 allow natural usage in combination with the ||>, ||>>, |-> and
  5665 fold_map combinators.
  5666 
  5667 * Pure: official theorem names (closed derivations) and additional
  5668 comments (tags) are now strictly separate.  Name hints -- which are
  5669 maintained as tags -- may be attached any time without affecting the
  5670 derivation.
  5671 
  5672 * Pure: primitive rule lift_rule now takes goal cterm instead of an
  5673 actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
  5674 achieve the old behaviour.
  5675 
  5676 * Pure: the "Goal" constant is now called "prop", supporting a
  5677 slightly more general idea of ``protecting'' meta-level rule
  5678 statements.
  5679 
  5680 * Pure: Logic.(un)varify only works in a global context, which is now
  5681 enforced instead of silently assumed.  INCOMPATIBILITY, may use
  5682 Logic.legacy_(un)varify as temporary workaround.
  5683 
  5684 * Pure: structure Name provides scalable operations for generating
  5685 internal variable names, notably Name.variants etc.  This replaces
  5686 some popular functions from term.ML:
  5687 
  5688   Term.variant		->  Name.variant
  5689   Term.variantlist	->  Name.variant_list
  5690   Term.invent_names	->  Name.invent_list
  5691 
  5692 Note that low-level renaming rarely occurs in new code -- operations
  5693 from structure Variable are used instead (see below).
  5694 
  5695 * Pure: structure Variable provides fundamental operations for proper
  5696 treatment of fixed/schematic variables in a context.  For example,
  5697 Variable.import introduces fixes for schematics of given facts and
  5698 Variable.export reverses the effect (up to renaming) -- this replaces
  5699 various freeze_thaw operations.
  5700 
  5701 * Pure: structure Goal provides simple interfaces for
  5702 init/conclude/finish and tactical prove operations (replacing former
  5703 Tactic.prove).  Goal.prove is the canonical way to prove results
  5704 within a given context; Goal.prove_global is a degraded version for
  5705 theory level goals, including a global Drule.standard.  Note that
  5706 OldGoals.prove_goalw_cterm has long been obsolete, since it is
  5707 ill-behaved in a local proof context (e.g. with local fixes/assumes or
  5708 in a locale context).
  5709 
  5710 * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.)
  5711 and type checking (Syntax.check_term etc.), with common combinations
  5712 (Syntax.read_term etc.). These supersede former Sign.read_term etc.
  5713 which are considered legacy and await removal.
  5714 
  5715 * Pure/Syntax: generic interfaces for type unchecking
  5716 (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
  5717 with common combinations (Syntax.pretty_term, Syntax.string_of_term
  5718 etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
  5719 available for convenience, but refer to the very same operations using
  5720 a mere theory instead of a full context.
  5721 
  5722 * Isar: simplified treatment of user-level errors, using exception
  5723 ERROR of string uniformly.  Function error now merely raises ERROR,
  5724 without any side effect on output channels.  The Isar toplevel takes
  5725 care of proper display of ERROR exceptions.  ML code may use plain
  5726 handle/can/try; cat_error may be used to concatenate errors like this:
  5727 
  5728   ... handle ERROR msg => cat_error msg "..."
  5729 
  5730 Toplevel ML code (run directly or through the Isar toplevel) may be
  5731 embedded into the Isar toplevel with exception display/debug like
  5732 this:
  5733 
  5734   Isar.toplevel (fn () => ...)
  5735 
  5736 INCOMPATIBILITY, removed special transform_error facilities, removed
  5737 obsolete variants of user-level exceptions (ERROR_MESSAGE,
  5738 Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
  5739 -- use plain ERROR instead.
  5740 
  5741 * Isar: theory setup now has type (theory -> theory), instead of a
  5742 list.  INCOMPATIBILITY, may use #> to compose setup functions.
  5743 
  5744 * Isar: ML toplevel pretty printer for type Proof.context, subject to
  5745 ProofContext.debug/verbose flags.
  5746 
  5747 * Isar: Toplevel.theory_to_proof admits transactions that modify the
  5748 theory before entering a proof state.  Transactions now always see a
  5749 quasi-functional intermediate checkpoint, both in interactive and
  5750 batch mode.
  5751 
  5752 * Isar: simplified interfaces for outer syntax.  Renamed
  5753 OuterSyntax.add_keywords to OuterSyntax.keywords.  Removed
  5754 OuterSyntax.add_parsers -- this functionality is now included in
  5755 OuterSyntax.command etc.  INCOMPATIBILITY.
  5756 
  5757 * Simplifier: the simpset of a running simplification process now
  5758 contains a proof context (cf. Simplifier.the_context), which is the
  5759 very context that the initial simpset has been retrieved from (by
  5760 simpset_of/local_simpset_of).  Consequently, all plug-in components
  5761 (solver, looper etc.) may depend on arbitrary proof data.
  5762 
  5763 * Simplifier.inherit_context inherits the proof context (plus the
  5764 local bounds) of the current simplification process; any simproc
  5765 etc. that calls the Simplifier recursively should do this!  Removed
  5766 former Simplifier.inherit_bounds, which is already included here --
  5767 INCOMPATIBILITY.  Tools based on low-level rewriting may even have to
  5768 specify an explicit context using Simplifier.context/theory_context.
  5769 
  5770 * Simplifier/Classical Reasoner: more abstract interfaces
  5771 change_simpset/claset for modifying the simpset/claset reference of a
  5772 theory; raw versions simpset/claset_ref etc. have been discontinued --
  5773 INCOMPATIBILITY.
  5774 
  5775 * Provers: more generic wrt. syntax of object-logics, avoid hardwired
  5776 "Trueprop" etc.
  5777 
  5778 
  5779 *** System ***
  5780 
  5781 * settings: the default heap location within ISABELLE_HOME_USER now
  5782 includes ISABELLE_IDENTIFIER.  This simplifies use of multiple
  5783 Isabelle installations.
  5784 
  5785 * isabelle-process: option -S (secure mode) disables some critical
  5786 operations, notably runtime compilation and evaluation of ML source
  5787 code.
  5788 
  5789 * Basic Isabelle mode for jEdit, see Isabelle/lib/jedit/.
  5790 
  5791 * Support for parallel execution, using native multicore support of
  5792 Poly/ML 5.1.  The theory loader exploits parallelism when processing
  5793 independent theories, according to the given theory header
  5794 specifications. The maximum number of worker threads is specified via
  5795 usedir option -M or the "max-threads" setting in Proof General. A
  5796 speedup factor of 1.5--3.5 can be expected on a 4-core machine, and up
  5797 to 6 on a 8-core machine.  User-code needs to observe certain
  5798 guidelines for thread-safe programming, see appendix A in the Isar
  5799 Implementation manual.
  5800 
  5801 
  5802 
  5803 New in Isabelle2005 (October 2005)
  5804 ----------------------------------
  5805 
  5806 *** General ***
  5807 
  5808 * Theory headers: the new header syntax for Isar theories is
  5809 
  5810   theory <name>
  5811   imports <theory1> ... <theoryN>
  5812   uses <file1> ... <fileM>
  5813   begin
  5814 
  5815 where the 'uses' part is optional.  The previous syntax
  5816 
  5817   theory <name> = <theory1> + ... + <theoryN>:
  5818 
  5819 will disappear in the next release.  Use isatool fixheaders to convert
  5820 existing theory files.  Note that there is no change in ancient
  5821 non-Isar theories now, but these will disappear soon.
  5822 
  5823 * Theory loader: parent theories can now also be referred to via
  5824 relative and absolute paths.
  5825 
  5826 * Command 'find_theorems' searches for a list of criteria instead of a
  5827 list of constants. Known criteria are: intro, elim, dest, name:string,
  5828 simp:term, and any term. Criteria can be preceded by '-' to select
  5829 theorems that do not match. Intro, elim, dest select theorems that
  5830 match the current goal, name:s selects theorems whose fully qualified
  5831 name contain s, and simp:term selects all simplification rules whose
  5832 lhs match term.  Any other term is interpreted as pattern and selects
  5833 all theorems matching the pattern. Available in ProofGeneral under
  5834 'ProofGeneral -> Find Theorems' or C-c C-f.  Example:
  5835 
  5836   C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."
  5837 
  5838 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
  5839 matching the current goal as introduction rule and not having "HOL."
  5840 in their name (i.e. not being defined in theory HOL).
  5841 
  5842 * Command 'thms_containing' has been discontinued in favour of
  5843 'find_theorems'; INCOMPATIBILITY.
  5844 
  5845 * Communication with Proof General is now 8bit clean, which means that
  5846 Unicode text in UTF-8 encoding may be used within theory texts (both
  5847 formal and informal parts).  Cf. option -U of the Isabelle Proof
  5848 General interface.  Here are some simple examples (cf. src/HOL/ex):
  5849 
  5850   http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html
  5851   http://isabelle.in.tum.de/library/HOL/ex/Chinese.html
  5852 
  5853 * Improved efficiency of the Simplifier and, to a lesser degree, the
  5854 Classical Reasoner.  Typical big applications run around 2 times
  5855 faster.
  5856 
  5857 
  5858 *** Document preparation ***
  5859 
  5860 * Commands 'display_drafts' and 'print_drafts' perform simple output
  5861 of raw sources.  Only those symbols that do not require additional
  5862 LaTeX packages (depending on comments in isabellesym.sty) are
  5863 displayed properly, everything else is left verbatim.  isatool display
  5864 and isatool print are used as front ends (these are subject to the
  5865 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
  5866 
  5867 * Command tags control specific markup of certain regions of text,
  5868 notably folding and hiding.  Predefined tags include "theory" (for
  5869 theory begin and end), "proof" for proof commands, and "ML" for
  5870 commands involving ML code; the additional tags "visible" and
  5871 "invisible" are unused by default.  Users may give explicit tag
  5872 specifications in the text, e.g. ''by %invisible (auto)''.  The
  5873 interpretation of tags is determined by the LaTeX job during document
  5874 preparation: see option -V of isatool usedir, or options -n and -t of
  5875 isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
  5876 \isadroptag.
  5877 
  5878 Several document versions may be produced at the same time via isatool
  5879 usedir (the generated index.html will link all of them).  Typical
  5880 specifications include ''-V document=theory,proof,ML'' to present
  5881 theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
  5882 proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
  5883 these parts without any formal replacement text.  The Isabelle site
  5884 default settings produce ''document'' and ''outline'' versions as
  5885 specified above.
  5886 
  5887 * Several new antiquotations:
  5888 
  5889   @{term_type term} prints a term with its type annotated;
  5890 
  5891   @{typeof term} prints the type of a term;
  5892 
  5893   @{const const} is the same as @{term const}, but checks that the
  5894   argument is a known logical constant;
  5895 
  5896   @{term_style style term} and @{thm_style style thm} print a term or
  5897   theorem applying a "style" to it
  5898 
  5899   @{ML text}
  5900 
  5901 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
  5902 definitions, equations, inequations etc., 'concl' printing only the
  5903 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19'
  5904 to print the specified premise.  TermStyle.add_style provides an ML
  5905 interface for introducing further styles.  See also the "LaTeX Sugar"
  5906 document practical applications.  The ML antiquotation prints
  5907 type-checked ML expressions verbatim.
  5908 
  5909 * Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
  5910 and 'text' support optional locale specification '(in loc)', which
  5911 specifies the default context for interpreting antiquotations.  For
  5912 example: 'text (in lattice) {* @{thm inf_assoc}*}'.
  5913 
  5914 * Option 'locale=NAME' of antiquotations specifies an alternative
  5915 context interpreting the subsequent argument.  For example: @{thm
  5916 [locale=lattice] inf_assoc}.
  5917 
  5918 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
  5919 a proof context.
  5920 
  5921 * Proper output of antiquotations for theory commands involving a
  5922 proof context (such as 'locale' or 'theorem (in loc) ...').
  5923 
  5924 * Delimiters of outer tokens (string etc.) now produce separate LaTeX
  5925 macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
  5926 
  5927 * isatool usedir: new option -C (default true) controls whether option
  5928 -D should include a copy of the original document directory; -C false
  5929 prevents unwanted effects such as copying of administrative CVS data.
  5930 
  5931 
  5932 *** Pure ***
  5933 
  5934 * Considerably improved version of 'constdefs' command.  Now performs
  5935 automatic type-inference of declared constants; additional support for
  5936 local structure declarations (cf. locales and HOL records), see also
  5937 isar-ref manual.  Potential INCOMPATIBILITY: need to observe strictly
  5938 sequential dependencies of definitions within a single 'constdefs'
  5939 section; moreover, the declared name needs to be an identifier.  If
  5940 all fails, consider to fall back on 'consts' and 'defs' separately.
  5941 
  5942 * Improved indexed syntax and implicit structures.  First of all,
  5943 indexed syntax provides a notational device for subscripted
  5944 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
  5945 expressions.  Secondly, in a local context with structure
  5946 declarations, number indexes \<^sub>n or the empty index (default
  5947 number 1) refer to a certain fixed variable implicitly; option
  5948 show_structs controls printing of implicit structures.  Typical
  5949 applications of these concepts involve record types and locales.
  5950 
  5951 * New command 'no_syntax' removes grammar declarations (and
  5952 translations) resulting from the given syntax specification, which is
  5953 interpreted in the same manner as for the 'syntax' command.
  5954 
  5955 * 'Advanced' translation functions (parse_translation etc.) may depend
  5956 on the signature of the theory context being presently used for
  5957 parsing/printing, see also isar-ref manual.
  5958 
  5959 * Improved 'oracle' command provides a type-safe interface to turn an
  5960 ML expression of type theory -> T -> term into a primitive rule of
  5961 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
  5962 is already included here); see also FOL/ex/IffExample.thy;
  5963 INCOMPATIBILITY.
  5964 
  5965 * axclass: name space prefix for class "c" is now "c_class" (was "c"
  5966 before); "cI" is no longer bound, use "c.intro" instead.
  5967 INCOMPATIBILITY.  This change avoids clashes of fact bindings for
  5968 axclasses vs. locales.
  5969 
  5970 * Improved internal renaming of symbolic identifiers -- attach primes
  5971 instead of base 26 numbers.
  5972 
  5973 * New flag show_question_marks controls printing of leading question
  5974 marks in schematic variable names.
  5975 
  5976 * In schematic variable names, *any* symbol following \<^isub> or
  5977 \<^isup> is now treated as part of the base name.  For example, the
  5978 following works without printing of awkward ".0" indexes:
  5979 
  5980   lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"
  5981     by simp
  5982 
  5983 * Inner syntax includes (*(*nested*) comments*).
  5984 
  5985 * Pretty printer now supports unbreakable blocks, specified in mixfix
  5986 annotations as "(00...)".
  5987 
  5988 * Clear separation of logical types and nonterminals, where the latter
  5989 may only occur in 'syntax' specifications or type abbreviations.
  5990 Before that distinction was only partially implemented via type class
  5991 "logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper
  5992 use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very
  5993 exotic syntax specifications may require further adaption
  5994 (e.g. Cube/Cube.thy).
  5995 
  5996 * Removed obsolete type class "logic", use the top sort {} instead.
  5997 Note that non-logical types should be declared as 'nonterminals'
  5998 rather than 'types'.  INCOMPATIBILITY for new object-logic
  5999 specifications.
  6000 
  6001 * Attributes 'induct' and 'cases': type or set names may now be
  6002 locally fixed variables as well.
  6003 
  6004 * Simplifier: can now control the depth to which conditional rewriting
  6005 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
  6006 Limit.
  6007 
  6008 * Simplifier: simplification procedures may now take the current
  6009 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
  6010 interface), which is very useful for calling the Simplifier
  6011 recursively.  Minor INCOMPATIBILITY: the 'prems' argument of simprocs
  6012 is gone -- use prems_of_ss on the simpset instead.  Moreover, the
  6013 low-level mk_simproc no longer applies Logic.varify internally, to
  6014 allow for use in a context of fixed variables.
  6015 
  6016 * thin_tac now works even if the assumption being deleted contains !!
  6017 or ==>.  More generally, erule now works even if the major premise of
  6018 the elimination rule contains !! or ==>.
  6019 
  6020 * Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY.
  6021 
  6022 * Reorganized bootstrapping of the Pure theories; CPure is now derived
  6023 from Pure, which contains all common declarations already.  Both
  6024 theories are defined via plain Isabelle/Isar .thy files.
  6025 INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
  6026 CPure.elim / CPure.dest attributes) now appear in the Pure name space;
  6027 use isatool fixcpure to adapt your theory and ML sources.
  6028 
  6029 * New syntax 'name(i-j, i-, i, ...)' for referring to specific
  6030 selections of theorems in named facts via index ranges.
  6031 
  6032 * 'print_theorems': in theory mode, really print the difference
  6033 wrt. the last state (works for interactive theory development only),
  6034 in proof mode print all local facts (cf. 'print_facts');
  6035 
  6036 * 'hide': option '(open)' hides only base names.
  6037 
  6038 * More efficient treatment of intermediate checkpoints in interactive
  6039 theory development.
  6040 
  6041 * Code generator is now invoked via code_module (incremental code
  6042 generation) and code_library (modular code generation, ML structures
  6043 for each theory).  INCOMPATIBILITY: new keywords 'file' and 'contains'
  6044 must be quoted when used as identifiers.
  6045 
  6046 * New 'value' command for reading, evaluating and printing terms using
  6047 the code generator.  INCOMPATIBILITY: command keyword 'value' must be
  6048 quoted when used as identifier.
  6049 
  6050 
  6051 *** Locales ***
  6052 
  6053 * New commands for the interpretation of locale expressions in
  6054 theories (1), locales (2) and proof contexts (3).  These generate
  6055 proof obligations from the expression specification.  After the
  6056 obligations have been discharged, theorems of the expression are added
  6057 to the theory, target locale or proof context.  The synopsis of the
  6058 commands is a follows:
  6059 
  6060   (1) interpretation expr inst
  6061   (2) interpretation target < expr
  6062   (3) interpret expr inst
  6063 
  6064 Interpretation in theories and proof contexts require a parameter
  6065 instantiation of terms from the current context.  This is applied to
  6066 specifications and theorems of the interpreted expression.
  6067 Interpretation in locales only permits parameter renaming through the
  6068 locale expression.  Interpretation is smart in that interpretations
  6069 that are active already do not occur in proof obligations, neither are
  6070 instantiated theorems stored in duplicate.  Use 'print_interps' to
  6071 inspect active interpretations of a particular locale.  For details,
  6072 see the Isar Reference manual.  Examples can be found in
  6073 HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy.
  6074 
  6075 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
  6076 'interpret' instead.
  6077 
  6078 * New context element 'constrains' for adding type constraints to
  6079 parameters.
  6080 
  6081 * Context expressions: renaming of parameters with syntax
  6082 redeclaration.
  6083 
  6084 * Locale declaration: 'includes' disallowed.
  6085 
  6086 * Proper static binding of attribute syntax -- i.e. types / terms /
  6087 facts mentioned as arguments are always those of the locale definition
  6088 context, independently of the context of later invocations.  Moreover,
  6089 locale operations (renaming and type / term instantiation) are applied
  6090 to attribute arguments as expected.
  6091 
  6092 INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of
  6093 actual attributes; rare situations may require Attrib.attribute to
  6094 embed those attributes into Attrib.src that lack concrete syntax.
  6095 Attribute implementations need to cooperate properly with the static
  6096 binding mechanism.  Basic parsers Args.XXX_typ/term/prop and
  6097 Attrib.XXX_thm etc. already do the right thing without further
  6098 intervention.  Only unusual applications -- such as "where" or "of"
  6099 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both
  6100 on the context and the facts involved -- may have to assign parsed
  6101 values to argument tokens explicitly.
  6102 
  6103 * Changed parameter management in theorem generation for long goal
  6104 statements with 'includes'.  INCOMPATIBILITY: produces a different
  6105 theorem statement in rare situations.
  6106 
  6107 * Locale inspection command 'print_locale' omits notes elements.  Use
  6108 'print_locale!' to have them included in the output.
  6109 
  6110 
  6111 *** Provers ***
  6112 
  6113 * Provers/hypsubst.ML: improved version of the subst method, for
  6114 single-step rewriting: it now works in bound variable contexts. New is
  6115 'subst (asm)', for rewriting an assumption.  INCOMPATIBILITY: may
  6116 rewrite a different subterm than the original subst method, which is
  6117 still available as 'simplesubst'.
  6118 
  6119 * Provers/quasi.ML: new transitivity reasoners for transitivity only
  6120 and quasi orders.
  6121 
  6122 * Provers/trancl.ML: new transitivity reasoner for transitive and
  6123 reflexive-transitive closure of relations.
  6124 
  6125 * Provers/blast.ML: new reference depth_limit to make blast's depth
  6126 limit (previously hard-coded with a value of 20) user-definable.
  6127 
  6128 * Provers/simplifier.ML has been moved to Pure, where Simplifier.setup
  6129 is peformed already.  Object-logics merely need to finish their
  6130 initial simpset configuration as before.  INCOMPATIBILITY.
  6131 
  6132 
  6133 *** HOL ***
  6134 
  6135 * Symbolic syntax of Hilbert Choice Operator is now as follows:
  6136 
  6137   syntax (epsilon)
  6138     "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
  6139 
  6140 The symbol \<some> is displayed as the alternative epsilon of LaTeX
  6141 and x-symbol; use option '-m epsilon' to get it actually printed.
  6142 Moreover, the mathematically important symbolic identifier \<epsilon>
  6143 becomes available as variable, constant etc.  INCOMPATIBILITY,
  6144 
  6145 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
  6146 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
  6147 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
  6148 support corresponding Isar calculations.
  6149 
  6150 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
  6151 instead of ":".
  6152 
  6153 * theory SetInterval: changed the syntax for open intervals:
  6154 
  6155   Old       New
  6156   {..n(}    {..<n}
  6157   {)n..}    {n<..}
  6158   {m..n(}   {m..<n}
  6159   {)m..n}   {m<..n}
  6160   {)m..n(}  {m<..<n}
  6161 
  6162 The old syntax is still supported but will disappear in the next
  6163 release.  For conversion use the following Emacs search and replace
  6164 patterns (these are not perfect but work quite well):
  6165 
  6166   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
  6167   \.\.\([^(}]*\)(}  ->  \.\.<\1}
  6168 
  6169 * Theory Commutative_Ring (in Library): method comm_ring for proving
  6170 equalities in commutative rings; method 'algebra' provides a generic
  6171 interface.
  6172 
  6173 * Theory Finite_Set: changed the syntax for 'setsum', summation over
  6174 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
  6175 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
  6176 be a tuple pattern.
  6177 
  6178 Some new syntax forms are available:
  6179 
  6180   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
  6181   "\<Sum>x = a..b. e"   for     "setsum (%x. e) {a..b}"
  6182   "\<Sum>x = a..<b. e"  for     "setsum (%x. e) {a..<b}"
  6183   "\<Sum>x < k. e"      for     "setsum (%x. e) {..<k}"
  6184 
  6185 The latter form "\<Sum>x < k. e" used to be based on a separate
  6186 function "Summation", which has been discontinued.
  6187 
  6188 * theory Finite_Set: in structured induction proofs, the insert case
  6189 is now 'case (insert x F)' instead of the old counterintuitive 'case
  6190 (insert F x)'.
  6191 
  6192 * The 'refute' command has been extended to support a much larger
  6193 fragment of HOL, including axiomatic type classes, constdefs and
  6194 typedefs, inductive datatypes and recursion.
  6195 
  6196 * New tactics 'sat' and 'satx' to prove propositional tautologies.
  6197 Requires zChaff with proof generation to be installed.  See
  6198 HOL/ex/SAT_Examples.thy for examples.
  6199 
  6200 * Datatype induction via method 'induct' now preserves the name of the
  6201 induction variable. For example, when proving P(xs::'a list) by
  6202 induction on xs, the induction step is now P(xs) ==> P(a#xs) rather
  6203 than P(list) ==> P(a#list) as previously.  Potential INCOMPATIBILITY
  6204 in unstructured proof scripts.
  6205 
  6206 * Reworked implementation of records.  Improved scalability for
  6207 records with many fields, avoiding performance problems for type
  6208 inference. Records are no longer composed of nested field types, but
  6209 of nested extension types. Therefore the record type only grows linear
  6210 in the number of extensions and not in the number of fields.  The
  6211 top-level (users) view on records is preserved.  Potential
  6212 INCOMPATIBILITY only in strange cases, where the theory depends on the
  6213 old record representation. The type generated for a record is called
  6214 <record_name>_ext_type.
  6215 
  6216 Flag record_quick_and_dirty_sensitive can be enabled to skip the
  6217 proofs triggered by a record definition or a simproc (if
  6218 quick_and_dirty is enabled).  Definitions of large records can take
  6219 quite long.
  6220 
  6221 New simproc record_upd_simproc for simplification of multiple record
  6222 updates enabled by default.  Moreover, trivial updates are also
  6223 removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
  6224 occasionally, since simplification is more powerful by default.
  6225 
  6226 * typedef: proper support for polymorphic sets, which contain extra
  6227 type-variables in the term.
  6228 
  6229 * Simplifier: automatically reasons about transitivity chains
  6230 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
  6231 provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY:
  6232 old proofs break occasionally as simplification may now solve more
  6233 goals than previously.
  6234 
  6235 * Simplifier: converts x <= y into x = y if assumption y <= x is
  6236 present.  Works for all partial orders (class "order"), in particular
  6237 numbers and sets.  For linear orders (e.g. numbers) it treats ~ x < y
  6238 just like y <= x.
  6239 
  6240 * Simplifier: new simproc for "let x = a in f x".  If a is a free or
  6241 bound variable or a constant then the let is unfolded.  Otherwise
  6242 first a is simplified to b, and then f b is simplified to g. If
  6243 possible we abstract b from g arriving at "let x = b in h x",
  6244 otherwise we unfold the let and arrive at g.  The simproc can be
  6245 enabled/disabled by the reference use_let_simproc.  Potential
  6246 INCOMPATIBILITY since simplification is more powerful by default.
  6247 
  6248 * Classical reasoning: the meson method now accepts theorems as arguments.
  6249 
  6250 * Prover support: pre-release of the Isabelle-ATP linkup, which runs background
  6251 jobs to provide advice on the provability of subgoals.
  6252 
  6253 * Theory OrderedGroup and Ring_and_Field: various additions and
  6254 improvements to faciliate calculations involving equalities and
  6255 inequalities.
  6256 
  6257 The following theorems have been eliminated or modified