misc tuning for release;
authorwenzelm
Mon Dec 31 13:08:37 2012 +0100 (2012-12-31)
changeset 50646c02e6a75aa3f
parent 50645 cb8f93361e86
child 50647 58312dae25a5
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Mon Dec 31 12:25:11 2012 +0100
     1.2 +++ b/NEWS	Mon Dec 31 13:08:37 2012 +0100
     1.3 @@ -102,17 +102,12 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Dropped legacy antiquotations "term_style" and "thm_style", since
     1.8 -styles may be given as arguments to "term" and "thm" already.  Dropped
     1.9 -legacy styles "prem1" .. "prem19".  INCOMPATIBILITY.
    1.10 -
    1.11  * Code generation for Haskell: restrict unqualified imports from
    1.12  Haskell Prelude to a small set of fundamental operations.
    1.13  
    1.14 -* Command "export_code": relative file names are interpreted
    1.15 -relatively to master directory of current theory rather than
    1.16 -the rather arbitrary current working directory.
    1.17 -INCOMPATIBILITY.
    1.18 +* Command 'export_code': relative file names are interpreted
    1.19 +relatively to master directory of current theory rather than the
    1.20 +rather arbitrary current working directory.  INCOMPATIBILITY.
    1.21  
    1.22  * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
    1.23  use regular rule composition via "OF" / "THEN", or explicit proof
    1.24 @@ -129,11 +124,34 @@
    1.25  
    1.26  *** HOL ***
    1.27  
    1.28 -* Removed constant "chars".  Prefer "Enum.enum" on type "char"
    1.29 -directly.  INCOMPATIBILITY.
    1.30 -
    1.31 -* Moved operation product, sublists and n_lists from Enum.thy
    1.32 -to List.thy.  INCOMPATIBILITY.
    1.33 +* Sledgehammer:
    1.34 +
    1.35 +  - Added MaSh relevance filter based on machine-learning; see the
    1.36 +    Sledgehammer manual for details.
    1.37 +  - Polished Isar proofs generated with "isar_proofs" option.
    1.38 +  - Rationalized type encodings ("type_enc" option).
    1.39 +  - Renamed "kill_provers" subcommand to "kill".
    1.40 +  - Renamed options:
    1.41 +      isar_proof ~> isar_proofs
    1.42 +      isar_shrink_factor ~> isar_shrink
    1.43 +      max_relevant ~> max_facts
    1.44 +      relevance_thresholds ~> fact_thresholds
    1.45 +
    1.46 +* Quickcheck: added an optimisation for equality premises.  It is
    1.47 +switched on by default, and can be switched off by setting the
    1.48 +configuration quickcheck_optimise_equality to false.
    1.49 +
    1.50 +* Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.51 +expressions.
    1.52 +
    1.53 +* Preprocessing of the code generator rewrites set comprehensions into
    1.54 +pointfree expressions.
    1.55 +
    1.56 +* The SMT solver Z3 has now by default a restricted set of directly
    1.57 +supported features. For the full set of features (div/mod, nonlinear
    1.58 +arithmetic, datatypes/records) with potential proof reconstruction
    1.59 +failures, enable the configuration option "z3_with_extensions".  Minor
    1.60 +INCOMPATIBILITY.
    1.61  
    1.62  * Simplified 'typedef' specifications: historical options for implicit
    1.63  set definition and alternative name have been discontinued.  The
    1.64 @@ -141,51 +159,84 @@
    1.65  written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
    1.66  accordingly.
    1.67  
    1.68 -* Theory "Library/Multiset":
    1.69 -
    1.70 -  - Renamed constants
    1.71 -      fold_mset ~> Multiset.fold  -- for coherence with other fold combinators
    1.72 -
    1.73 -  - Renamed facts
    1.74 -      fold_mset_commute ~> fold_mset_comm  -- for coherence with fold_comm
    1.75 -
    1.76 -INCOMPATIBILITY.
    1.77 +* Removed constant "chars"; prefer "Enum.enum" on type "char"
    1.78 +directly.  INCOMPATIBILITY.
    1.79 +
    1.80 +* Moved operation product, sublists and n_lists from theory Enum to
    1.81 +List.  INCOMPATIBILITY.
    1.82  
    1.83  * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
    1.84  
    1.85  * Class "comm_monoid_diff" formalises properties of bounded
    1.86  subtraction, with natural numbers and multisets as typical instances.
    1.87  
    1.88 -* Theory "Library/Option_ord" provides instantiation of option type
    1.89 -to lattice type classes.
    1.90 -
    1.91 -* New combinator "Option.these" with type "'a option set => 'a set".
    1.92 -
    1.93 -* Renamed theory Library/List_Prefix to Library/Sublist.
    1.94 -INCOMPATIBILITY.  Related changes are:
    1.95 -
    1.96 -  - Renamed constants:
    1.97 +* Added combinator "Option.these" with type "'a option set => 'a set".
    1.98 +
    1.99 +* Theory "Transitive_Closure": renamed lemmas
   1.100 +
   1.101 +  reflcl_tranclp -> reflclp_tranclp
   1.102 +  rtranclp_reflcl -> rtranclp_reflclp
   1.103 +
   1.104 +INCOMPATIBILITY.
   1.105 +
   1.106 +* Theory "Rings": renamed lemmas (in class semiring)
   1.107 +
   1.108 +  left_distrib ~> distrib_right
   1.109 +  right_distrib ~> distrib_left
   1.110 +
   1.111 +INCOMPATIBILITY.
   1.112 +
   1.113 +* Generalized the definition of limits:
   1.114 +
   1.115 +  - Introduced the predicate filterlim (LIM x F. f x :> G) which
   1.116 +    expresses that when the input values x converge to F then the
   1.117 +    output f x converges to G.
   1.118 +
   1.119 +  - Added filters for convergence to positive (at_top) and negative
   1.120 +    infinity (at_bot).
   1.121 +
   1.122 +  - Moved infinity in the norm (at_infinity) from
   1.123 +    Multivariate_Analysis to Complex_Main.
   1.124 +
   1.125 +  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>
   1.126 +    at_top".
   1.127 +
   1.128 +INCOMPATIBILITY.
   1.129 +
   1.130 +* Theory "Library/Option_ord" provides instantiation of option type to
   1.131 +lattice type classes.
   1.132 +
   1.133 +* Theory "Library/Multiset": renamed
   1.134 +
   1.135 +    constant fold_mset ~> Multiset.fold
   1.136 +    fact fold_mset_commute ~> fold_mset_comm
   1.137 +
   1.138 +INCOMPATIBILITY.
   1.139 +
   1.140 +* Renamed theory Library/List_Prefix to Library/Sublist, with related
   1.141 +changes as follows.
   1.142 +
   1.143 +  - Renamed constants (and related lemmas)
   1.144  
   1.145        prefix ~> prefixeq
   1.146        strict_prefix ~> prefix
   1.147  
   1.148 -    Renamed lemmas accordingly, INCOMPATIBILITY.
   1.149 -
   1.150 -  - Replaced constant "postfix" by "suffixeq" with swapped argument order
   1.151 -    (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix
   1.152 -    syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
   1.153 -    accordingly.  INCOMPATIBILITY.
   1.154 -
   1.155 -  - New constant "list_hembeq" for homeomorphic embedding on lists. New
   1.156 -    abbreviation "sublisteq" for special case "list_hembeq (op =)".
   1.157 -
   1.158 -  - Library/Sublist does no longer provide "order" and "bot" type class
   1.159 -    instances for the prefix order (merely corresponding locale
   1.160 -    interpretations). The type class instances are to be found in
   1.161 -    Library/Prefix_Order. INCOMPATIBILITY.
   1.162 -
   1.163 -  - The sublist relation from Library/Sublist_Order is now based on
   1.164 -    "Sublist.sublisteq". Replaced lemmas:
   1.165 +  - Replaced constant "postfix" by "suffixeq" with swapped argument
   1.166 +    order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped
   1.167 +    old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.
   1.168 +    Renamed lemmas accordingly.
   1.169 +
   1.170 +  - Added constant "list_hembeq" for homeomorphic embedding on
   1.171 +    lists. Added abbreviation "sublisteq" for special case
   1.172 +    "list_hembeq (op =)".
   1.173 +
   1.174 +  - Theory Library/Sublist no longer provides "order" and "bot" type
   1.175 +    class instances for the prefix order (merely corresponding locale
   1.176 +    interpretations). The type class instances are now in theory
   1.177 +    Library/Prefix_Order.
   1.178 +
   1.179 +  - The sublist relation of theory Library/Sublist_Order is now based
   1.180 +    on "Sublist.sublisteq".  Renamed lemmas accordingly:
   1.181  
   1.182        le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
   1.183        le_list_append_mono ~> Sublist.list_hembeq_append_mono
   1.184 @@ -204,148 +255,110 @@
   1.185        less_eq_list.induct ~> less_eq_list_induct
   1.186        not_le_list_length ~> Sublist.not_sublisteq_length
   1.187  
   1.188 -    INCOMPATIBILITY.
   1.189 -
   1.190 -* Further generalized the definition of limits:
   1.191 -
   1.192 -  - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that
   1.193 -    when the input values x converge to F then the output f x converges to G.
   1.194 -
   1.195 -  - Added filters for convergence to positive (at_top) and negative infinity (at_bot).
   1.196 -    Moved infinity in the norm (at_infinity) from Multivariate_Analysis to Complex_Main.
   1.197 -
   1.198 -  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
   1.199 -    INCOMPATIBILITY
   1.200 -
   1.201 -* HOL/Transitive_Closure: renamed lemmas
   1.202 -  reflcl_tranclp -> reflclp_tranclp
   1.203 -  rtranclp_reflcl -> rtranclp_reflclp
   1.204 -
   1.205 -* HOL/Rings: renamed lemmas
   1.206 -
   1.207 -left_distrib ~> distrib_right
   1.208 -right_distrib ~> distrib_left
   1.209 -
   1.210 -in class semiring.  INCOMPATIBILITY.
   1.211 -
   1.212 -* HOL/BNF: New (co)datatype package based on bounded natural
   1.213 -functors with support for mixed, nested recursion and interesting
   1.214 -non-free datatypes.
   1.215 -
   1.216 -* HOL/Cardinals: Theories of ordinals and cardinals
   1.217 -(supersedes the AFP entry "Ordinals_and_Cardinals").
   1.218 -
   1.219 -* HOL/Multivariate_Analysis:
   1.220 -  Replaced "basis :: 'a::euclidean_space => nat => real" and
   1.221 -  "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space" on euclidean spaces by
   1.222 -  using the inner product "_ \<bullet> _" with vectors from the Basis set.
   1.223 -  "\<Chi>\<Chi> i. f i" is replaced by "SUM i : Basis. f i *r i".
   1.224 -
   1.225 -  With this change the following constants are also chanegd or removed:
   1.226 -
   1.227 -    DIM('a) :: nat   ~>   card (Basis :: 'a set)   (is an abbreviation)
   1.228 -    a $$ i    ~>    inner a i  (where i : Basis)
   1.229 -    cart_base i     removed
   1.230 -    \<pi>, \<pi>'   removed
   1.231 +INCOMPATIBILITY.
   1.232 +
   1.233 +
   1.234 +* New theory Library/Countable_Set.
   1.235 +
   1.236 +* Theory Library/Debug and Library/Parallel provide debugging and
   1.237 +parallel execution for code generated towards Isabelle/ML.
   1.238 +
   1.239 +* Theory Library/FuncSet: Extended support for Pi and extensional and
   1.240 +introduce the extensional dependent function space "PiE". Replaced
   1.241 +extensional_funcset by an abbreviation, and renamed lemmas from
   1.242 +extensional_funcset to PiE as follows:
   1.243 +
   1.244 +  extensional_empty  ~>  PiE_empty
   1.245 +  extensional_funcset_empty_domain  ~>  PiE_empty_domain
   1.246 +  extensional_funcset_empty_range  ~>  PiE_empty_range
   1.247 +  extensional_funcset_arb  ~>  PiE_arb
   1.248 +  extensional_funcset_mem  ~>  PiE_mem
   1.249 +  extensional_funcset_extend_domainI  ~>  PiE_fun_upd
   1.250 +  extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE
   1.251 +  extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq
   1.252 +  card_extensional_funcset  ~>  card_PiE
   1.253 +  finite_extensional_funcset  ~>  finite_PiE
   1.254 +
   1.255 +INCOMPATIBILITY.
   1.256 +
   1.257 +* Theory Library/FinFun: theory of almost everywhere constant
   1.258 +functions (supersedes the AFP entry "Code Generation for Functions as
   1.259 +Data").
   1.260 +
   1.261 +* Theory Library/Phantom: generic phantom type to make a type
   1.262 +parameter appear in a constant's type.  This alternative to adding
   1.263 +TYPE('a) as another parameter avoids unnecessary closures in generated
   1.264 +code.
   1.265 +
   1.266 +* Theory Library/RBT_Impl: efficient construction of red-black trees
   1.267 +from sorted associative lists. Merging two trees with rbt_union may
   1.268 +return a structurally different tree than before.  Potential
   1.269 +INCOMPATIBILITY.
   1.270 +
   1.271 +* Theory Library/IArray: immutable arrays with code generation.
   1.272 +
   1.273 +* Theory Library/Finite_Lattice: theory of finite lattices.
   1.274 +
   1.275 +* HOL/Multivariate_Analysis: replaced
   1.276 +
   1.277 +  "basis :: 'a::euclidean_space => nat => real"
   1.278 +  "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"
   1.279 +
   1.280 +on euclidean spaces by using the inner product "_ \<bullet> _" with
   1.281 +vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by
   1.282 +"SUM i : Basis. f i * r i".
   1.283 +
   1.284 +  With this change the following constants are also changed or removed:
   1.285 +
   1.286 +    DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)
   1.287 +    a $$ i  ~>  inner a i  (where i : Basis)
   1.288 +    cart_base i  removed
   1.289 +    \<pi>, \<pi>'  removed
   1.290  
   1.291    Theorems about these constants where removed.
   1.292  
   1.293    Renamed lemmas:
   1.294  
   1.295 -    component_le_norm   ~>   Basis_le_norm
   1.296 -    euclidean_eq   ~>   euclidean_eq_iff
   1.297 -    differential_zero_maxmin_component   ~>   differential_zero_maxmin_cart
   1.298 -    euclidean_simps   ~>   inner_simps
   1.299 -    independent_basis   ~>   independent_Basis
   1.300 -    span_basis   ~>   span_Basis
   1.301 -    in_span_basis   ~>   in_span_Basis
   1.302 -    norm_bound_component_le   ~>   norm_boound_Basis_le
   1.303 -    norm_bound_component_lt   ~>   norm_boound_Basis_lt
   1.304 -    component_le_infnorm   ~>   Basis_le_infnorm
   1.305 -
   1.306 -  INCOMPATIBILITY.
   1.307 +    component_le_norm  ~>  Basis_le_norm
   1.308 +    euclidean_eq  ~>  euclidean_eq_iff
   1.309 +    differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart
   1.310 +    euclidean_simps  ~>  inner_simps
   1.311 +    independent_basis  ~>  independent_Basis
   1.312 +    span_basis  ~>  span_Basis
   1.313 +    in_span_basis  ~>  in_span_Basis
   1.314 +    norm_bound_component_le  ~>  norm_boound_Basis_le
   1.315 +    norm_bound_component_lt  ~>  norm_boound_Basis_lt
   1.316 +    component_le_infnorm  ~>  Basis_le_infnorm
   1.317 +
   1.318 +INCOMPATIBILITY.
   1.319  
   1.320  * HOL/Probability:
   1.321 -  - Add simproc "measurable" to automatically prove measurability
   1.322 -
   1.323 -  - Add induction rules for sigma sets with disjoint union (sigma_sets_induct_disjoint)
   1.324 -    and for Borel-measurable functions (borel_measurable_induct).
   1.325 -
   1.326 -  - The Daniell-Kolmogorov theorem (the existence the limit of a projective family)
   1.327 -
   1.328 -* Library/Countable_Set.thy: Theory of countable sets.
   1.329 -
   1.330 -* Library/Debug.thy and Library/Parallel.thy: debugging and parallel
   1.331 -execution for code generated towards Isabelle/ML.
   1.332 -
   1.333 -* Library/FuncSet.thy: Extended support for Pi and extensional and introduce the
   1.334 -extensional dependent function space "PiE". Replaces extensional_funcset by an
   1.335 -abbreviation, rename a couple of lemmas from extensional_funcset to PiE:
   1.336 -
   1.337 -      extensional_empty ~> PiE_empty
   1.338 -      extensional_funcset_empty_domain ~> PiE_empty_domain
   1.339 -      extensional_funcset_empty_range ~> PiE_empty_range
   1.340 -      extensional_funcset_arb ~> PiE_arb
   1.341 -      extensional_funcset_mem > PiE_mem
   1.342 -      extensional_funcset_extend_domainI ~> PiE_fun_upd
   1.343 -      extensional_funcset_restrict_domain ~> fun_upd_in_PiE
   1.344 -      extensional_funcset_extend_domain_eq ~> PiE_insert_eq
   1.345 -      card_extensional_funcset ~> card_PiE
   1.346 -      finite_extensional_funcset ~> finite_PiE
   1.347 -
   1.348 -  INCOMPATIBILITY.
   1.349 -
   1.350 -* Library/FinFun.thy: theory of almost everywhere constant functions
   1.351 -(supersedes the AFP entry "Code Generation for Functions as Data").
   1.352 -
   1.353 -* Library/Phantom.thy: generic phantom type to make a type parameter
   1.354 -appear in a constant's type. This alternative to adding TYPE('a) as
   1.355 -another parameter avoids unnecessary closures in generated code.
   1.356 -
   1.357 -* Library/RBT_Impl.thy: efficient construction of red-black trees 
   1.358 -from sorted associative lists. Merging two trees with rbt_union may
   1.359 -return a structurally different tree than before. MINOR INCOMPATIBILITY.
   1.360 -
   1.361 -* Library/IArray.thy: immutable arrays with code generation.
   1.362 -
   1.363 -* Library/Finite_Lattice.thy: theory of finite lattices
   1.364 -
   1.365 -* Simproc "finite_Collect" rewrites set comprehensions into pointfree
   1.366 -expressions.
   1.367 -
   1.368 -* Preprocessing of the code generator rewrites set comprehensions into
   1.369 -pointfree expressions.
   1.370 -
   1.371 -* Quickcheck:
   1.372 -
   1.373 -  - added an optimisation for equality premises.
   1.374 -    It is switched on by default, and can be switched off by setting
   1.375 -    the configuration quickcheck_optimise_equality to false.
   1.376 -
   1.377 -* The SMT solver Z3 has now by default a restricted set of directly
   1.378 -supported features. For the full set of features (div/mod, nonlinear
   1.379 -arithmetic, datatypes/records) with potential proof reconstruction
   1.380 -failures, enable the configuration option "z3_with_extensions".
   1.381 -Minor INCOMPATIBILITY.
   1.382 -
   1.383 -* Sledgehammer:
   1.384 -
   1.385 -  - Added MaSh relevance filter based on machine-learning; see the
   1.386 -    Sledgehammer manual for details.
   1.387 -  - Polished Isar proofs generated with "isar_proofs" option.
   1.388 -  - Rationalized type encodings ("type_enc" option).
   1.389 -  - Renamed "kill_provers" subcommand to "kill".
   1.390 -  - Renamed options:
   1.391 -      isar_proof ~> isar_proofs
   1.392 -      isar_shrink_factor ~> isar_shrink
   1.393 -      max_relevant ~> max_facts
   1.394 -      relevance_thresholds ~> fact_thresholds
   1.395 +
   1.396 +  - Added simproc "measurable" to automatically prove measurability.
   1.397 +
   1.398 +  - Added induction rules for sigma sets with disjoint union
   1.399 +    (sigma_sets_induct_disjoint) and for Borel-measurable functions
   1.400 +    (borel_measurable_induct).
   1.401 +
   1.402 +  - Added the Daniell-Kolmogorov theorem (the existence the limit of a
   1.403 +    projective family).
   1.404 +
   1.405 +* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the
   1.406 +AFP entry "Ordinals_and_Cardinals").
   1.407 +
   1.408 +* HOL/BNF: New (co)datatype package based on bounded natural functors
   1.409 +with support for mixed, nested recursion and interesting non-free
   1.410 +datatypes.
   1.411  
   1.412  
   1.413  *** Document preparation ***
   1.414  
   1.415 -* Default for \<euro> is now based on eurosym package, instead of
   1.416 -slightly exotic babel/greek.
   1.417 +* Dropped legacy antiquotations "term_style" and "thm_style", since
   1.418 +styles may be given as arguments to "term" and "thm" already.
   1.419 +Discontinued legacy styles "prem1" .. "prem19".
   1.420 +
   1.421 +* Default LaTeX rendering for \<euro> is now based on eurosym package,
   1.422 +instead of slightly exotic babel/greek.
   1.423  
   1.424  * Document variant NAME may use different LaTeX entry point
   1.425  document/root_NAME.tex if that file exists, instead of the common
   1.426 @@ -357,6 +370,10 @@
   1.427  
   1.428  *** ML ***
   1.429  
   1.430 +* The default limit for maximum number of worker threads is now 8,
   1.431 +instead of 4, in correspondence to capabilities of contemporary
   1.432 +hardware and Poly/ML runtime system.
   1.433 +
   1.434  * Type Seq.results and related operations support embedded error
   1.435  messages within lazy enumerations, and thus allow to provide
   1.436  informative errors in the absence of any usable results.
   1.437 @@ -368,16 +385,6 @@
   1.438  
   1.439  *** System ***
   1.440  
   1.441 -* The default limit for maximum number of worker threads is now 8,
   1.442 -instead of 4.
   1.443 -
   1.444 -* The ML system is configured as regular component, and no longer
   1.445 -picked up from some surrounding directory.  Potential INCOMPATIBILITY
   1.446 -for home-made configurations.
   1.447 -
   1.448 -* The "isabelle logo" tool produces EPS and PDF format simultaneously.
   1.449 -Minor INCOMPATIBILITY in command-line options.
   1.450 -
   1.451  * Advanced support for Isabelle sessions and build management, see
   1.452  "system" manual for the chapter of that name, especially the "isabelle
   1.453  build" tool and its examples.  INCOMPATIBILITY, isabelle usedir /
   1.454 @@ -403,12 +410,22 @@
   1.455  with "isabelle build", similar to former "isabelle mkdir" for
   1.456  "isabelle usedir".
   1.457  
   1.458 +* The "isabelle logo" tool produces EPS and PDF format simultaneously.
   1.459 +Minor INCOMPATIBILITY in command-line options.
   1.460 +
   1.461 +* The "isabelle install" tool has now a simpler command-line.  Minor
   1.462 +INCOMPATIBILITY.
   1.463 +
   1.464  * The "isabelle components" tool helps to resolve add-on components
   1.465  that are not bundled, or referenced from a bare-bones repository
   1.466  version of Isabelle.
   1.467  
   1.468 -* The "isabelle install" tool has now a simpler command-line.  Minor
   1.469 -INCOMPATIBILITY.
   1.470 +* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general
   1.471 +platform family: "linux", "macos", "windows".
   1.472 +
   1.473 +* The ML system is configured as regular component, and no longer
   1.474 +picked up from some surrounding directory.  Potential INCOMPATIBILITY
   1.475 +for home-made settings.
   1.476  
   1.477  * Discontinued support for Poly/ML 5.2.1, which was the last version
   1.478  without exception positions and advanced ML compiler/toplevel
   1.479 @@ -420,8 +437,6 @@
   1.480  settings manually, or use a Proof General version that has been
   1.481  bundled as Isabelle component.
   1.482  
   1.483 -* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general
   1.484 -platform family: "linux", "macos", "windows".
   1.485  
   1.486  
   1.487  New in Isabelle2012 (May 2012)