1.1 --- a/NEWS Wed Apr 04 09:59:49 2012 +0200
1.2 +++ b/NEWS Mon Apr 16 19:01:57 2012 +0200
1.3 @@ -1,8 +1,8 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 -New in this Isabelle version
1.8 -----------------------------
1.9 +New in Isabelle2012 (May 2012)
1.10 +------------------------------
1.11
1.12 *** General ***
1.13
1.14 @@ -47,12 +47,46 @@
1.15 header -- minor INCOMPATIBILITY for user-defined commands. Allow new
1.16 commands to be used in the same theory where defined.
1.17
1.18 -* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
1.19 -(not just JRE).
1.20 -
1.21
1.22 *** Pure ***
1.23
1.24 +* Auxiliary contexts indicate block structure for specifications with
1.25 +additional parameters and assumptions. Such unnamed contexts may be
1.26 +nested within other targets, like 'theory', 'locale', 'class',
1.27 +'instantiation' etc. Results from the local context are generalized
1.28 +accordingly and applied to the enclosing target context. Example:
1.29 +
1.30 + context
1.31 + fixes x y z :: 'a
1.32 + assumes xy: "x = y" and yz: "y = z"
1.33 + begin
1.34 +
1.35 + lemma my_trans: "x = z" using xy yz by simp
1.36 +
1.37 + end
1.38 +
1.39 + thm my_trans
1.40 +
1.41 +The most basic application is to factor-out context elements of
1.42 +several fixes/assumes/shows theorem statements, e.g. see
1.43 +~~/src/HOL/Isar_Examples/Group_Context.thy
1.44 +
1.45 +Any other local theory specification element works within the "context
1.46 +... begin ... end" block as well.
1.47 +
1.48 +* Bundled declarations associate attributed fact expressions with a
1.49 +given name in the context. These may be later included in other
1.50 +contexts. This allows to manage context extensions casually, without
1.51 +the logical dependencies of locales and locale interpretation.
1.52 +
1.53 +See commands 'bundle', 'include', 'including' etc. in the isar-ref
1.54 +manual.
1.55 +
1.56 +* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
1.57 +tolerant against multiple unifiers, as long as the final result is
1.58 +unique. (As before, rules are composed in canonical right-to-left
1.59 +order to accommodate newly introduced premises.)
1.60 +
1.61 * Command 'definition' no longer exports the foundational "raw_def"
1.62 into the user context. Minor INCOMPATIBILITY, may use the regular
1.63 "def" result with attribute "abs_def" to imitate the old version.
1.64 @@ -63,21 +97,21 @@
1.65 undocumented feature.)
1.66
1.67 * Discontinued old "prems" fact, which used to refer to the accidental
1.68 -collection of foundational premises in the context (marked as legacy
1.69 -since Isabelle2011).
1.70 +collection of foundational premises in the context (already marked as
1.71 +legacy since Isabelle2011).
1.72
1.73 * Obsolete command 'types' has been discontinued. Use 'type_synonym'
1.74 instead. INCOMPATIBILITY.
1.75
1.76 -* Ancient code generator for SML and its commands 'code_module',
1.77 +* Old code generator for SML and its commands 'code_module',
1.78 'code_library', 'consts_code', 'types_code' have been discontinued.
1.79 Use commands of the generic code generator instead. INCOMPATIBILITY.
1.80
1.81 -* Redundant attribute 'code_inline' has been discontinued. Use
1.82 -'code_unfold' instead. INCOMPATIBILITY.
1.83 -
1.84 -* Dropped attribute 'code_unfold_post' in favor of the its dual
1.85 -'code_abbrev', which yields a common pattern in definitions like
1.86 +* Redundant attribute "code_inline" has been discontinued. Use
1.87 +"code_unfold" instead. INCOMPATIBILITY.
1.88 +
1.89 +* Dropped attribute "code_unfold_post" in favor of the its dual
1.90 +"code_abbrev", which yields a common pattern in definitions like
1.91
1.92 definition [code_abbrev]: "f = t"
1.93
1.94 @@ -90,17 +124,20 @@
1.95 lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal"
1.96
1.97 lemma "P (x::'a)" and "Q (y::'a::bar)"
1.98 - -- "now uniform 'a::bar instead of default sort for first occurence (!)"
1.99 + -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
1.100
1.101
1.102 *** HOL ***
1.103
1.104 -* New tutorial "Programming and Proving in Isabelle/HOL".
1.105 +
1.106 +* New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").
1.107 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
1.108 which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
1.109 for Higher-Order Logic" as the recommended beginners tutorial
1.110 but does not cover all of the material of that old tutorial.
1.111
1.112 +* Discontinued old Tutorial on Isar ("isar-overview");
1.113 +
1.114 * The representation of numerals has changed. We now have a datatype
1.115 "num" representing strictly positive binary numerals, along with
1.116 functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
1.117 @@ -131,19 +168,44 @@
1.118 sets separate, it is often sufficient to rephrase sets S accidentally
1.119 used as predicates by "%x. x : S" and predicates P accidentally used
1.120 as sets by "{x. P x}". Corresponding proofs in a first step should be
1.121 -pruned from any tinkering with former theorems mem_def and
1.122 -Collect_def as far as possible.
1.123 -For developments which deliberately mixed predicates and
1.124 -sets, a planning step is necessary to determine what should become a
1.125 -predicate and what a set. It can be helpful to carry out that step in
1.126 +pruned from any tinkering with former theorems mem_def and Collect_def
1.127 +as far as possible.
1.128 +
1.129 +For developments which deliberately mixed predicates and sets, a
1.130 +planning step is necessary to determine what should become a predicate
1.131 +and what a set. It can be helpful to carry out that step in
1.132 Isabelle2011-1 before jumping right into the current release.
1.133
1.134 +* The representation of numerals has changed. Datatype "num"
1.135 +represents strictly positive binary numerals, along with functions
1.136 +"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
1.137 +positive and negated numeric literals, respectively. (See definitions
1.138 +in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories
1.139 +may require adaptations as follows:
1.140 +
1.141 + - Theorems with number_ring or number_semiring constraints: These
1.142 + classes are gone; use comm_ring_1 or comm_semiring_1 instead.
1.143 +
1.144 + - Theories defining numeric types: Remove number, number_semiring,
1.145 + and number_ring instances. Defer all theorems about numerals until
1.146 + after classes one and semigroup_add have been instantiated.
1.147 +
1.148 + - Numeral-only simp rules: Replace each rule having a "number_of v"
1.149 + pattern with two copies, one for numeral and one for neg_numeral.
1.150 +
1.151 + - Theorems about subclasses of semiring_1 or ring_1: These classes
1.152 + automatically support numerals now, so more simp rules and
1.153 + simprocs may now apply within the proof.
1.154 +
1.155 + - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
1.156 + Redefine using other integer operations.
1.157 +
1.158 * Code generation by default implements sets as container type rather
1.159 than predicates. INCOMPATIBILITY.
1.160
1.161 * New proof import from HOL Light: Faster, simpler, and more scalable.
1.162 Requires a proof bundle, which is available as an external component.
1.163 -Removed old (and mostly dead) Importer for HOL4 and HOL Light.
1.164 +Discontinued old (and mostly dead) Importer for HOL4 and HOL Light.
1.165 INCOMPATIBILITY.
1.166
1.167 * New type synonym 'a rel = ('a * 'a) set
1.168 @@ -177,8 +239,8 @@
1.169 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
1.170
1.171 * More default pred/set conversions on a couple of relation operations
1.172 -and predicates. Added powers of predicate relations.
1.173 -Consolidation of some relation theorems:
1.174 +and predicates. Added powers of predicate relations. Consolidation
1.175 +of some relation theorems:
1.176
1.177 converse_def ~> converse_unfold
1.178 rel_comp_def ~> rel_comp_unfold
1.179 @@ -189,8 +251,8 @@
1.180
1.181 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
1.182
1.183 -See theory "Relation" for examples for making use of pred/set conversions
1.184 -by means of attributes "to_set" and "to_pred".
1.185 +See theory "Relation" for examples for making use of pred/set
1.186 +conversions by means of attributes "to_set" and "to_pred".
1.187
1.188 INCOMPATIBILITY.
1.189
1.190 @@ -212,10 +274,11 @@
1.191 SUPR_set_fold ~> SUP_set_fold
1.192 INF_code ~> INF_set_foldr
1.193 SUP_code ~> SUP_set_foldr
1.194 - foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
1.195 - foldl.simps ~> foldl_Nil foldl_Cons
1.196 - foldr_fold_rev ~> foldr_def
1.197 - foldl_fold ~> foldl_def
1.198 + foldr.simps ~> foldr.simps (in point-free formulation)
1.199 + foldr_fold_rev ~> foldr_conv_fold
1.200 + foldl_fold ~> foldl_conv_fold
1.201 + foldr_foldr ~> foldr_conv_foldl
1.202 + foldl_foldr ~> foldl_conv_foldr
1.203
1.204 INCOMPATIBILITY.
1.205
1.206 @@ -224,11 +287,19 @@
1.207 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
1.208 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
1.209 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
1.210 -listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY.
1.211 -Prefer "List.fold" with canonical argument order, or boil down
1.212 -"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"
1.213 -and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0"
1.214 -and "List.foldl plus 0", prefer "List.listsum".
1.215 +listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
1.216 +foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
1.217 +INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"
1.218 +and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be
1.219 +useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
1.220 +unfolding "foldr_conv_fold" and "foldl_conv_fold".
1.221 +
1.222 +* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
1.223 +inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
1.224 +Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
1.225 +INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding
1.226 +lemmas over fold rather than foldr, or make use of lemmas
1.227 +fold_conv_foldr and fold_rev.
1.228
1.229 * Congruence rules Option.map_cong and Option.bind_cong for recursion
1.230 through option types.
1.231 @@ -255,8 +326,8 @@
1.232 INCOMPATIBILITY.
1.233
1.234 * Renamed facts about the power operation on relations, i.e., relpow
1.235 - to match the constant's name:
1.236 -
1.237 +to match the constant's name:
1.238 +
1.239 rel_pow_1 ~> relpow_1
1.240 rel_pow_0_I ~> relpow_0_I
1.241 rel_pow_Suc_I ~> relpow_Suc_I
1.242 @@ -265,7 +336,7 @@
1.243 rel_pow_Suc_E ~> relpow_Suc_E
1.244 rel_pow_E ~> relpow_E
1.245 rel_pow_Suc_D2 ~> relpow_Suc_D2
1.246 - rel_pow_Suc_E2 ~> relpow_Suc_E2
1.247 + rel_pow_Suc_E2 ~> relpow_Suc_E2
1.248 rel_pow_Suc_D2' ~> relpow_Suc_D2'
1.249 rel_pow_E2 ~> relpow_E2
1.250 rel_pow_add ~> relpow_add
1.251 @@ -281,17 +352,167 @@
1.252 rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow
1.253 trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow
1.254 single_valued_rel_pow ~> single_valued_relpow
1.255 -
1.256 +
1.257 INCOMPATIBILITY.
1.258
1.259 -* New theory HOL/Library/DAList provides an abstract type for association
1.260 - lists with distinct keys.
1.261 +* Theory Relation: Consolidated constant name for relation composition
1.262 +and corresponding theorem names:
1.263 +
1.264 + - Renamed constant rel_comp to relcomp
1.265 +
1.266 + - Dropped abbreviation pred_comp. Use relcompp instead.
1.267 +
1.268 + - Renamed theorems:
1.269 +
1.270 + rel_compI ~> relcompI
1.271 + rel_compEpair ~> relcompEpair
1.272 + rel_compE ~> relcompE
1.273 + pred_comp_rel_comp_eq ~> relcompp_relcomp_eq
1.274 + rel_comp_empty1 ~> relcomp_empty1
1.275 + rel_comp_mono ~> relcomp_mono
1.276 + rel_comp_subset_Sigma ~> relcomp_subset_Sigma
1.277 + rel_comp_distrib ~> relcomp_distrib
1.278 + rel_comp_distrib2 ~> relcomp_distrib2
1.279 + rel_comp_UNION_distrib ~> relcomp_UNION_distrib
1.280 + rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
1.281 + single_valued_rel_comp ~> single_valued_relcomp
1.282 + rel_comp_unfold ~> relcomp_unfold
1.283 + converse_rel_comp ~> converse_relcomp
1.284 + pred_compI ~> relcomppI
1.285 + pred_compE ~> relcomppE
1.286 + pred_comp_bot1 ~> relcompp_bot1
1.287 + pred_comp_bot2 ~> relcompp_bot2
1.288 + transp_pred_comp_less_eq ~> transp_relcompp_less_eq
1.289 + pred_comp_mono ~> relcompp_mono
1.290 + pred_comp_distrib ~> relcompp_distrib
1.291 + pred_comp_distrib2 ~> relcompp_distrib2
1.292 + converse_pred_comp ~> converse_relcompp
1.293 +
1.294 + finite_rel_comp ~> finite_relcomp
1.295 +
1.296 + set_rel_comp ~> set_relcomp
1.297 +
1.298 +INCOMPATIBILITY.
1.299 +
1.300 +* New theory HOL/Library/DAList provides an abstract type for
1.301 +association lists with distinct keys.
1.302
1.303 * 'datatype' specifications allow explicit sort constraints.
1.304
1.305 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
1.306 use theory HOL/Library/Nat_Bijection instead.
1.307
1.308 +* Theory HOL/Library/RBT_Impl: Backing implementation of red-black
1.309 +trees is now inside a type class context. Names of affected
1.310 +operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for
1.311 +theories working directly with raw red-black trees, adapt the names as
1.312 +follows:
1.313 +
1.314 + Operations:
1.315 + bulkload -> rbt_bulkload
1.316 + del_from_left -> rbt_del_from_left
1.317 + del_from_right -> rbt_del_from_right
1.318 + del -> rbt_del
1.319 + delete -> rbt_delete
1.320 + ins -> rbt_ins
1.321 + insert -> rbt_insert
1.322 + insertw -> rbt_insert_with
1.323 + insert_with_key -> rbt_insert_with_key
1.324 + map_entry -> rbt_map_entry
1.325 + lookup -> rbt_lookup
1.326 + sorted -> rbt_sorted
1.327 + tree_greater -> rbt_greater
1.328 + tree_less -> rbt_less
1.329 + tree_less_symbol -> rbt_less_symbol
1.330 + union -> rbt_union
1.331 + union_with -> rbt_union_with
1.332 + union_with_key -> rbt_union_with_key
1.333 +
1.334 + Lemmas:
1.335 + balance_left_sorted -> balance_left_rbt_sorted
1.336 + balance_left_tree_greater -> balance_left_rbt_greater
1.337 + balance_left_tree_less -> balance_left_rbt_less
1.338 + balance_right_sorted -> balance_right_rbt_sorted
1.339 + balance_right_tree_greater -> balance_right_rbt_greater
1.340 + balance_right_tree_less -> balance_right_rbt_less
1.341 + balance_sorted -> balance_rbt_sorted
1.342 + balance_tree_greater -> balance_rbt_greater
1.343 + balance_tree_less -> balance_rbt_less
1.344 + bulkload_is_rbt -> rbt_bulkload_is_rbt
1.345 + combine_sorted -> combine_rbt_sorted
1.346 + combine_tree_greater -> combine_rbt_greater
1.347 + combine_tree_less -> combine_rbt_less
1.348 + delete_in_tree -> rbt_delete_in_tree
1.349 + delete_is_rbt -> rbt_delete_is_rbt
1.350 + del_from_left_tree_greater -> rbt_del_from_left_rbt_greater
1.351 + del_from_left_tree_less -> rbt_del_from_left_rbt_less
1.352 + del_from_right_tree_greater -> rbt_del_from_right_rbt_greater
1.353 + del_from_right_tree_less -> rbt_del_from_right_rbt_less
1.354 + del_in_tree -> rbt_del_in_tree
1.355 + del_inv1_inv2 -> rbt_del_inv1_inv2
1.356 + del_sorted -> rbt_del_rbt_sorted
1.357 + del_tree_greater -> rbt_del_rbt_greater
1.358 + del_tree_less -> rbt_del_rbt_less
1.359 + dom_lookup_Branch -> dom_rbt_lookup_Branch
1.360 + entries_lookup -> entries_rbt_lookup
1.361 + finite_dom_lookup -> finite_dom_rbt_lookup
1.362 + insert_sorted -> rbt_insert_rbt_sorted
1.363 + insertw_is_rbt -> rbt_insertw_is_rbt
1.364 + insertwk_is_rbt -> rbt_insertwk_is_rbt
1.365 + insertwk_sorted -> rbt_insertwk_rbt_sorted
1.366 + insertw_sorted -> rbt_insertw_rbt_sorted
1.367 + ins_sorted -> ins_rbt_sorted
1.368 + ins_tree_greater -> ins_rbt_greater
1.369 + ins_tree_less -> ins_rbt_less
1.370 + is_rbt_sorted -> is_rbt_rbt_sorted
1.371 + lookup_balance -> rbt_lookup_balance
1.372 + lookup_bulkload -> rbt_lookup_rbt_bulkload
1.373 + lookup_delete -> rbt_lookup_rbt_delete
1.374 + lookup_Empty -> rbt_lookup_Empty
1.375 + lookup_from_in_tree -> rbt_lookup_from_in_tree
1.376 + lookup_in_tree -> rbt_lookup_in_tree
1.377 + lookup_ins -> rbt_lookup_ins
1.378 + lookup_insert -> rbt_lookup_rbt_insert
1.379 + lookup_insertw -> rbt_lookup_rbt_insertw
1.380 + lookup_insertwk -> rbt_lookup_rbt_insertwk
1.381 + lookup_keys -> rbt_lookup_keys
1.382 + lookup_map -> rbt_lookup_map
1.383 + lookup_map_entry -> rbt_lookup_rbt_map_entry
1.384 + lookup_tree_greater -> rbt_lookup_rbt_greater
1.385 + lookup_tree_less -> rbt_lookup_rbt_less
1.386 + lookup_union -> rbt_lookup_rbt_union
1.387 + map_entry_color_of -> rbt_map_entry_color_of
1.388 + map_entry_inv1 -> rbt_map_entry_inv1
1.389 + map_entry_inv2 -> rbt_map_entry_inv2
1.390 + map_entry_is_rbt -> rbt_map_entry_is_rbt
1.391 + map_entry_sorted -> rbt_map_entry_rbt_sorted
1.392 + map_entry_tree_greater -> rbt_map_entry_rbt_greater
1.393 + map_entry_tree_less -> rbt_map_entry_rbt_less
1.394 + map_tree_greater -> map_rbt_greater
1.395 + map_tree_less -> map_rbt_less
1.396 + map_sorted -> map_rbt_sorted
1.397 + paint_sorted -> paint_rbt_sorted
1.398 + paint_lookup -> paint_rbt_lookup
1.399 + paint_tree_greater -> paint_rbt_greater
1.400 + paint_tree_less -> paint_rbt_less
1.401 + sorted_entries -> rbt_sorted_entries
1.402 + tree_greater_eq_trans -> rbt_greater_eq_trans
1.403 + tree_greater_nit -> rbt_greater_nit
1.404 + tree_greater_prop -> rbt_greater_prop
1.405 + tree_greater_simps -> rbt_greater_simps
1.406 + tree_greater_trans -> rbt_greater_trans
1.407 + tree_less_eq_trans -> rbt_less_eq_trans
1.408 + tree_less_nit -> rbt_less_nit
1.409 + tree_less_prop -> rbt_less_prop
1.410 + tree_less_simps -> rbt_less_simps
1.411 + tree_less_trans -> rbt_less_trans
1.412 + tree_ord_props -> rbt_ord_props
1.413 + union_Branch -> rbt_union_Branch
1.414 + union_is_rbt -> rbt_union_is_rbt
1.415 + unionw_is_rbt -> rbt_unionw_is_rbt
1.416 + unionwk_is_rbt -> rbt_unionwk_is_rbt
1.417 + unionwk_sorted -> rbt_unionwk_rbt_sorted
1.418 +
1.419 * Session HOL-Word: Discontinued many redundant theorems specific to
1.420 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
1.421 instead.
1.422 @@ -398,36 +619,45 @@
1.423 produces a rule which can be used to perform case distinction on both
1.424 a list and a nat.
1.425
1.426 -* Improved code generation of multisets.
1.427 -
1.428 -* New diagnostic command find_unused_assms to find potentially superfluous
1.429 - assumptions in theorems using Quickcheck.
1.430 +* Theory Library/Multiset: Improved code generation of multisets.
1.431 +
1.432 +* New diagnostic command 'find_unused_assms' to find potentially
1.433 +superfluous assumptions in theorems using Quickcheck.
1.434
1.435 * Quickcheck:
1.436 +
1.437 - Quickcheck returns variable assignments as counterexamples, which
1.438 allows to reveal the underspecification of functions under test.
1.439 For example, refuting "hd xs = x", it presents the variable
1.440 assignment xs = [] and x = a1 as a counterexample, assuming that
1.441 any property is false whenever "hd []" occurs in it.
1.442 +
1.443 These counterexample are marked as potentially spurious, as
1.444 Quickcheck also returns "xs = []" as a counterexample to the
1.445 obvious theorem "hd xs = hd xs".
1.446 +
1.447 After finding a potentially spurious counterexample, Quickcheck
1.448 continues searching for genuine ones.
1.449 +
1.450 By default, Quickcheck shows potentially spurious and genuine
1.451 - counterexamples. The option "genuine_only" sets quickcheck to
1.452 - only show genuine counterexamples.
1.453 + counterexamples. The option "genuine_only" sets quickcheck to only
1.454 + show genuine counterexamples.
1.455
1.456 - The command 'quickcheck_generator' creates random and exhaustive
1.457 value generators for a given type and operations.
1.458 +
1.459 It generates values by using the operations as if they were
1.460 - constructors of that type.
1.461 + constructors of that type.
1.462
1.463 - Support for multisets.
1.464
1.465 - Added "use_subtype" options.
1.466 -
1.467 +
1.468 + - Added "quickcheck_locale" configuration to specify how to process
1.469 + conjectures in a locale context.
1.470 +
1.471 * Nitpick:
1.472 +
1.473 - Fixed infinite loop caused by the 'peephole_optim' option and
1.474 affecting 'rat' and 'real'.
1.475
1.476 @@ -442,12 +672,15 @@
1.477
1.478 * SMT:
1.479 - renamed "smt_fixed" option to "smt_read_only_certificates".
1.480 -
1.481 +
1.482 * Command 'try0':
1.483 - Renamed from 'try_methods'. INCOMPATIBILITY.
1.484
1.485 * New "eventually_elim" method as a generalized variant of the
1.486 - eventually_elim* rules. Supports structured proofs.
1.487 +eventually_elim* rules. Supports structured proofs.
1.488 +
1.489 +* HOL/TPTP: support to parse and import TPTP problems (all languages)
1.490 +into Isabelle/HOL.
1.491
1.492
1.493 *** FOL ***
1.494 @@ -455,6 +688,16 @@
1.495 * New "case_product" attribute (see HOL).
1.496
1.497
1.498 +*** ZF ***
1.499 +
1.500 +* Greater support for structured proofs involving induction or case
1.501 +analysis.
1.502 +
1.503 +* Much greater use of mathematical symbols.
1.504 +
1.505 +* Removal of many ML theorem bindings. INCOMPATIBILITY.
1.506 +
1.507 +
1.508 *** ML ***
1.509
1.510 * Antiquotation @{keyword "name"} produces a parser for outer syntax
1.511 @@ -503,6 +746,15 @@
1.512 delsplits ~> Splitter.del_split
1.513
1.514
1.515 +*** System ***
1.516 +
1.517 +* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
1.518 +(not just JRE).
1.519 +
1.520 +* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name
1.521 +notation, which is useful for the jEdit file browser, for example.
1.522 +
1.523 +
1.524
1.525 New in Isabelle2011-1 (October 2011)
1.526 ------------------------------------
1.527 @@ -1811,13 +2063,6 @@
1.528 * All constant names are now qualified internally and use proper
1.529 identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.
1.530
1.531 -*** ZF ***
1.532 -
1.533 -* Greater support for structured proofs involving induction or case analysis.
1.534 -
1.535 -* Much greater use of special symbols.
1.536 -
1.537 -* Removal of many ML theorem bindings. INCOMPATIBILITY.
1.538
1.539 *** ML ***
1.540
1.541 @@ -4909,7 +5154,7 @@
1.542 * HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY.
1.543
1.544 * HOL-Word: New extensive library and type for generic, fixed size
1.545 -machine words, with arithmetic, bit-wise, shifting and rotating
1.546 +machine words, with arithemtic, bit-wise, shifting and rotating
1.547 operations, reflection into int, nat, and bool lists, automation for
1.548 linear arithmetic (by automatic reflection into nat or int), including
1.549 lemmas on overflow and monotonicity. Instantiated to all appropriate