summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)