NEWS
changeset 57504 5cf245c62c4c
parent 57503 3e04e25a751e
child 57508 19240ff4b02d
     1.1 --- a/NEWS	Fri Jul 04 11:39:34 2014 +0200
     1.2 +++ b/NEWS	Fri Jul 04 14:52:05 2014 +0200
     1.3 @@ -15,6 +15,16 @@
     1.4  separate environments.  See also ~~/src/Tools/SML/Examples.thy for
     1.5  some examples.
     1.6  
     1.7 +* Standard tactics and proof methods such as "clarsimp", "auto" and
     1.8 +"safe" now preserve equality hypotheses "x = expr" where x is a free
     1.9 +variable.  Locale assumptions and chained facts containing "x"
    1.10 +continue to be useful.  The new method "hypsubst_thin" and the
    1.11 +configuration option "hypsubst_thin" (within the attribute name space)
    1.12 +restore the previous behavior.  INCOMPATIBILITY, especially where
    1.13 +induction is done after these methods or when the names of free and
    1.14 +bound variables clash.  As first approximation, old proofs may be
    1.15 +repaired by "using [[hypsubst_thin = true]]" in the critical spot.
    1.16 +
    1.17  * More static checking of proof methods, which allows the system to
    1.18  form a closure over the concrete syntax.  Method arguments should be
    1.19  processed in the original proof context as far as possible, before
    1.20 @@ -51,18 +61,6 @@
    1.21  * Updated and extended manuals: codegen, datatypes, implementation,
    1.22  isar-ref, jedit, system.
    1.23  
    1.24 -* Standard tactics and proof methods such as "clarsimp", "auto" and
    1.25 -"safe" now preserve equality hypotheses "x = expr" where x is a free
    1.26 -variable.  Locale assumptions and chained facts containing "x"
    1.27 -continue to be useful.  The new method "hypsubst_thin" and the
    1.28 -configuration option "hypsubst_thin" (within the attribute name space)
    1.29 -restore the previous behavior.
    1.30 -
    1.31 -INCOMPATIBILITY, especially where induction is done after these
    1.32 -methods or when the names of free and bound variables clash.  As first
    1.33 -approximation, old proofs may be repaired by "using [[hypsubst_thin =
    1.34 -true]]" in the critical spot.
    1.35 -
    1.36  
    1.37  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.38  
    1.39 @@ -122,9 +120,18 @@
    1.40  within the context.
    1.41  
    1.42  
    1.43 -
    1.44  *** Pure ***
    1.45  
    1.46 +* Low-level type-class commands 'classes', 'classrel', 'arities' have
    1.47 +been discontinued to avoid the danger of non-trivial axiomatization
    1.48 +that is not immediately visible.  INCOMPATIBILITY, use regular
    1.49 +'instance' command with proof.  The required OFCLASS(...) theorem
    1.50 +might be postulated via 'axiomatization' beforehand, or the proof
    1.51 +finished trivially if the underlying class definition is made vacuous
    1.52 +(without any assumptions).  See also Isabelle/ML operations
    1.53 +Axclass.class_axiomatization, Axclass.classrel_axiomatization,
    1.54 +Axclass.arity_axiomatization.
    1.55 +
    1.56  * Basic constants of Pure use more conventional names and are always
    1.57  qualified.  Rare INCOMPATIBILITY, but with potentially serious
    1.58  consequences, notably for tools in Isabelle/ML.  The following
    1.59 @@ -153,16 +160,6 @@
    1.60  Later the application is moved to the current Isabelle version, and
    1.61  the auxiliary aliases are deleted.
    1.62  
    1.63 -* Low-level type-class commands 'classes', 'classrel', 'arities' have
    1.64 -been discontinued to avoid the danger of non-trivial axiomatization
    1.65 -that is not immediately visible.  INCOMPATIBILITY, use regular
    1.66 -'instance' command with proof.  The required OFCLASS(...) theorem
    1.67 -might be postulated via 'axiomatization' beforehand, or the proof
    1.68 -finished trivially if the underlying class definition is made vacuous
    1.69 -(without any assumptions).  See also Isabelle/ML operations
    1.70 -Axclass.class_axiomatization, Axclass.classrel_axiomatization,
    1.71 -Axclass.arity_axiomatization.
    1.72 -
    1.73  * Attributes "where" and "of" allow an optional context of local
    1.74  variables ('for' declaration): these variables become schematic in the
    1.75  instantiated theorem.
    1.76 @@ -186,22 +183,45 @@
    1.77  (only makes sense in practice, if outer syntax is delimited
    1.78  differently, e.g. via cartouches).
    1.79  
    1.80 +* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
    1.81 +but the latter is retained some time as Proof General legacy.
    1.82 +
    1.83  * Code generator preprocessor: explicit control of simp tracing on a
    1.84  per-constant basis.  See attribute "code_preproc".
    1.85  
    1.86 -* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
    1.87 -but the latter is retained some time as Proof General legacy.
    1.88 -
    1.89  
    1.90  *** HOL ***
    1.91  
    1.92 -* Qualified String.implode and String.explode.  INCOMPATIBILITY.
    1.93 +* Code generator: enforce case of identifiers only for strict target
    1.94 +language requirements.  INCOMPATIBILITY.
    1.95 +
    1.96 +* Code generator: explicit proof contexts in many ML interfaces.
    1.97 +INCOMPATIBILITY.
    1.98 +
    1.99 +* Code generator: minimize exported identifiers by default.  Minor
   1.100 +INCOMPATIBILITY.
   1.101 +
   1.102 +* Code generation for SML and OCaml: dropped arcane "no_signatures"
   1.103 +option.  Minor INCOMPATIBILITY.
   1.104 +
   1.105 +* "declare [[code abort: ...]]" replaces "code_abort ...".
   1.106 +INCOMPATIBILITY.
   1.107 +
   1.108 +* "declare [[code drop: ...]]" drops all code equations associated
   1.109 +with the given constants.
   1.110 +
   1.111 +* Code generations are provided for make, fields, extend and truncate
   1.112 +operations on records.
   1.113  
   1.114  * Command and antiquotation "value" are now hardcoded against nbe and
   1.115  ML.  Minor INCOMPATIBILITY.
   1.116  
   1.117 -* Separate command "approximate" for approximative computation in
   1.118 -src/HOL/Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   1.119 +* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
   1.120 +
   1.121 +* The symbol "\<newline>" may be used within char or string literals
   1.122 +to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
   1.123 +
   1.124 +* Qualified String.implode and String.explode.  INCOMPATIBILITY.
   1.125  
   1.126  * Adjustion of INF and SUP operations:
   1.127    - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   1.128 @@ -217,13 +237,6 @@
   1.129  
   1.130  INCOMPATIBILITY.
   1.131  
   1.132 -* Revisions to HOL/Number_Theory
   1.133 -  - consolidated the proofs of the binomial theorem
   1.134 -  - the function fib is again of type nat=>nat and not overloaded
   1.135 -  - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
   1.136 -
   1.137 -INCOMPATIBILITY.
   1.138 -
   1.139  * Swapped orientation of facts image_comp and vimage_comp:
   1.140  
   1.141    image_compose ~> image_comp [symmetric]
   1.142 @@ -239,25 +252,6 @@
   1.143  [[simp_legacy_precond]].  This configuration option will disappear
   1.144  again in the future.  INCOMPATIBILITY.
   1.145  
   1.146 -* HOL-Word:
   1.147 -  - Abandoned fact collection "word_arith_alts", which is a duplicate
   1.148 -    of "word_arith_wis".
   1.149 -  - Dropped first (duplicated) element in fact collections
   1.150 -    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   1.151 -    "uint_word_arith_bintrs".
   1.152 -
   1.153 -* Code generator: enforce case of identifiers only for strict target
   1.154 -language requirements.  INCOMPATIBILITY.
   1.155 -
   1.156 -* Code generator: explicit proof contexts in many ML interfaces.
   1.157 -INCOMPATIBILITY.
   1.158 -
   1.159 -* Code generator: minimize exported identifiers by default.  Minor
   1.160 -INCOMPATIBILITY.
   1.161 -
   1.162 -* Code generation for SML and OCaml: dropped arcane "no_signatures"
   1.163 -option.  Minor INCOMPATIBILITY.
   1.164 -
   1.165  * Simproc "finite_Collect" is no longer enabled by default, due to
   1.166  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
   1.167  
   1.168 @@ -374,12 +368,8 @@
   1.169  
   1.170  INCOMPATIBILITY.
   1.171  
   1.172 -* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   1.173 -
   1.174 -* New theory src/HOL/Library/Tree.thy.
   1.175 -
   1.176 -* Theory reorganization:
   1.177 -  Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   1.178 +* Theory reorganization: split of Big_Operators.thy into
   1.179 +Groups_Big.thy and Lattices_Big.thy.
   1.180  
   1.181  * Consolidated some facts about big group operators:
   1.182  
   1.183 @@ -486,22 +476,11 @@
   1.184  
   1.185  * Try0: Added 'algebra' and 'meson' to the set of proof methods.
   1.186  
   1.187 -* Command renaming: enriched_type ~> functor. INCOMPATIBILITY.
   1.188 -
   1.189 -* The symbol "\<newline>" may be used within char or string literals
   1.190 -to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
   1.191 -
   1.192  * Activation of Z3 now works via "z3_non_commercial" system option
   1.193  (without requiring restart), instead of former settings variable
   1.194  "Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
   1.195  Plugin Options / Isabelle / General.
   1.196  
   1.197 -* "declare [[code abort: ...]]" replaces "code_abort ...".
   1.198 -INCOMPATIBILITY.
   1.199 -
   1.200 -* "declare [[code drop: ...]]" drops all code equations associated
   1.201 -with the given constants.
   1.202 -
   1.203  * Abolished slightly odd global lattice interpretation for min/max.
   1.204  
   1.205    Fact consolidations:
   1.206 @@ -557,15 +536,9 @@
   1.207  
   1.208  INCOMPATBILITY.
   1.209  
   1.210 -* HOL-Word: bit representations prefer type bool over type bit.
   1.211 -INCOMPATIBILITY.
   1.212 -
   1.213  * Theorem disambiguation Inf_le_Sup (on finite sets) ~>
   1.214  Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
   1.215  
   1.216 -* Code generations are provided for make, fields, extend and truncate
   1.217 -operations on records.
   1.218 -
   1.219  * Qualified constant names Wellfounded.acc, Wellfounded.accp.
   1.220  INCOMPATIBILITY.
   1.221  
   1.222 @@ -633,9 +606,6 @@
   1.223  
   1.224  * SUP and INF generalized to conditionally_complete_lattice.
   1.225  
   1.226 -* Theory Lubs moved HOL image to HOL-Library. It is replaced by
   1.227 -Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   1.228 -
   1.229  * Introduce bdd_above and bdd_below in theory
   1.230  Conditionally_Complete_Lattices, use them instead of explicitly
   1.231  stating boundedness of sets.
   1.232 @@ -764,6 +734,34 @@
   1.233    - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
   1.234      "hide_types".
   1.235  
   1.236 +* Theory Lubs moved HOL image to HOL-Library. It is replaced by
   1.237 +Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   1.238 +
   1.239 +* HOL-Library: new theory src/HOL/Library/Tree.thy.
   1.240 +
   1.241 +* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
   1.242 +is subsumed by session Kleene_Algebra in AFP.
   1.243 +
   1.244 +* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   1.245 +
   1.246 +* HOL-Word: bit representations prefer type bool over type bit.
   1.247 +INCOMPATIBILITY.
   1.248 +
   1.249 +* HOL-Word:
   1.250 +  - Abandoned fact collection "word_arith_alts", which is a duplicate
   1.251 +    of "word_arith_wis".
   1.252 +  - Dropped first (duplicated) element in fact collections
   1.253 +    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   1.254 +    "uint_word_arith_bintrs".
   1.255 +
   1.256 +* HOL-Number_Theory:
   1.257 +  - consolidated the proofs of the binomial theorem
   1.258 +  - the function fib is again of type nat => nat and not overloaded
   1.259 +  - no more references to Old_Number_Theory in the HOL libraries
   1.260 +    (except the AFP)
   1.261 +
   1.262 +INCOMPATIBILITY.
   1.263 +
   1.264  * HOL-Multivariate_Analysis:
   1.265    - Type class ordered_real_vector for ordered vector spaces.
   1.266    - New theory Complex_Basic_Analysis defining complex derivatives,
   1.267 @@ -908,8 +906,9 @@
   1.268    - Formalized properties about exponentially, Erlang, and normal
   1.269      distributed random variables.
   1.270  
   1.271 -* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by
   1.272 -session Kleene_Algebra in AFP.
   1.273 +* HOL-Decision_Procs: Separate command 'approximate' for approximative
   1.274 +computation in src/HOL/Decision_Procs/Approximation.  Minor
   1.275 +INCOMPATIBILITY.
   1.276  
   1.277  
   1.278  *** Scala ***
   1.279 @@ -926,6 +925,25 @@
   1.280  
   1.281  *** ML ***
   1.282  
   1.283 +* Subtle change of semantics of Thm.eq_thm: theory stamps are not
   1.284 +compared (according to Thm.thm_ord), but assumed to be covered by the
   1.285 +current background theory.  Thus equivalent data produced in different
   1.286 +branches of the theory graph usually coincides (e.g. relevant for
   1.287 +theory merge).  Note that the softer Thm.eq_thm_prop is often more
   1.288 +appropriate than Thm.eq_thm.
   1.289 +
   1.290 +* Proper context for basic Simplifier operations: rewrite_rule,
   1.291 +rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
   1.292 +pass runtime Proof.context (and ensure that the simplified entity
   1.293 +actually belongs to it).
   1.294 +
   1.295 +* Proper context discipline for read_instantiate and instantiate_tac:
   1.296 +variables that are meant to become schematic need to be given as
   1.297 +fixed, and are generalized by the explicit context of local variables.
   1.298 +This corresponds to Isar attributes "where" and "of" with 'for'
   1.299 +declaration.  INCOMPATIBILITY, also due to potential change of indices
   1.300 +of schematic variables.
   1.301 +
   1.302  * Moved ML_Compiler.exn_trace and other operations on exceptions to
   1.303  structure Runtime.  Minor INCOMPATIBILITY.
   1.304  
   1.305 @@ -941,30 +959,11 @@
   1.306  ML is still available as default_print_depth, but rarely used.  Minor
   1.307  INCOMPATIBILITY.
   1.308  
   1.309 -* Proper context discipline for read_instantiate and instantiate_tac:
   1.310 -variables that are meant to become schematic need to be given as
   1.311 -fixed, and are generalized by the explicit context of local variables.
   1.312 -This corresponds to Isar attributes "where" and "of" with 'for'
   1.313 -declaration.  INCOMPATIBILITY, also due to potential change of indices
   1.314 -of schematic variables.
   1.315 -
   1.316  * Toplevel function "use" refers to raw ML bootstrap environment,
   1.317  without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
   1.318  Note that 'ML_file' is the canonical command to load ML files into the
   1.319  formal context.
   1.320  
   1.321 -* Proper context for basic Simplifier operations: rewrite_rule,
   1.322 -rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
   1.323 -pass runtime Proof.context (and ensure that the simplified entity
   1.324 -actually belongs to it).
   1.325 -
   1.326 -* Subtle change of semantics of Thm.eq_thm: theory stamps are not
   1.327 -compared (according to Thm.thm_ord), but assumed to be covered by the
   1.328 -current background theory.  Thus equivalent data produced in different
   1.329 -branches of the theory graph usually coincides (e.g. relevant for
   1.330 -theory merge).  Note that the softer Thm.eq_thm_prop is often more
   1.331 -appropriate than Thm.eq_thm.
   1.332 -
   1.333  * Simplified programming interface to define ML antiquotations, see
   1.334  structure ML_Antiquotation.  Minor INCOMPATIBILITY.
   1.335  
   1.336 @@ -985,17 +984,17 @@
   1.337  *** System ***
   1.338  
   1.339  * Proof General with its traditional helper scripts is now an optional
   1.340 -Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
   1.341 -component repository http://isabelle.in.tum.de/components/.  See also
   1.342 -the "system" manual for general explanations about add-on components,
   1.343 -notably those that are not bundled with the normal release.
   1.344 +Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
   1.345 +component repository http://isabelle.in.tum.de/components/.  Note that
   1.346 +the "system" manual provides general explanations about add-on
   1.347 +components, especially those that are not bundled with the release.
   1.348  
   1.349  * The raw Isabelle process executable has been renamed from
   1.350  "isabelle-process" to "isabelle_process", which conforms to common
   1.351  shell naming conventions, and allows to define a shell function within
   1.352  the Isabelle environment to avoid dynamic path lookup.  Rare
   1.353 -incompatibility for old tools that do not use the $ISABELLE_PROCESS
   1.354 -settings variable yet.
   1.355 +incompatibility for old tools that do not use the ISABELLE_PROCESS
   1.356 +settings variable.
   1.357  
   1.358  * Former "isabelle tty" has been superseded by "isabelle console",
   1.359  with implicit build like "isabelle jedit", and without the mostly
   1.360 @@ -1018,14 +1017,14 @@
   1.361  repeated invocation in PIDE front-end: re-use single file
   1.362  $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   1.363  
   1.364 -* Windows: support for regular TeX installation (e.g. MiKTeX) instead
   1.365 -of TeX Live from Cygwin.
   1.366 -
   1.367  * Session ROOT specifications require explicit 'document_files' for
   1.368  robust dependencies on LaTeX sources.  Only these explicitly given
   1.369  files are copied to the document output directory, before document
   1.370  processing is started.
   1.371  
   1.372 +* Windows: support for regular TeX installation (e.g. MiKTeX) instead
   1.373 +of TeX Live from Cygwin.
   1.374 +
   1.375  
   1.376  
   1.377  New in Isabelle2013-2 (December 2013)