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

NEWS

changeset 57452 | ecad2a53755a |

parent 57443 | 577f029fde39 |

child 57474 | 250decee4ac5 |

1.1 --- a/NEWS Tue Jul 01 14:05:05 2014 +0200 1.2 +++ b/NEWS Tue Jul 01 14:52:08 2014 +0200 1.3 @@ -1,32 +1,19 @@ 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 Isabelle2014 (August 2014) 1.10 +--------------------------------- 1.11 1.12 *** General *** 1.13 1.14 -* Document antiquotation @{url} produces markup for the given URL, 1.15 -which results in an active hyperlink within the text. 1.16 - 1.17 -* Document antiquotation @{file_unchecked} is like @{file}, but does 1.18 -not check existence within the file-system. 1.19 - 1.20 -* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML 1.21 -workaround in Isabelle2013-1. The prover process no longer accepts 1.22 -old identifier syntax with \<^isub> or \<^isup>. 1.23 - 1.24 -* Syntax of document antiquotation @{rail} now uses \<newline> instead 1.25 -of "\\", to avoid the optical illusion of escaped backslash within 1.26 -string token. Minor INCOMPATIBILITY. 1.27 - 1.28 -* Lexical syntax (inner and outer) supports text cartouches with 1.29 -arbitrary nesting, and without escapes of quotes etc. The Prover IDE 1.30 -supports input via ` (backquote). 1.31 - 1.32 -* The outer syntax categories "text" (for formal comments and document 1.33 -markup commands) and "altstring" (for literal fact references) allow 1.34 -cartouches as well, in addition to the traditional mix of quotations. 1.35 +* Support for official Standard ML within the Isabelle context. 1.36 +Command 'SML_file' reads and evaluates the given Standard ML file. 1.37 +Toplevel bindings are stored within the theory context; the initial 1.38 +environment is restricted to the Standard ML implementation of 1.39 +Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' 1.40 +and 'SML_export' allow to exchange toplevel bindings between the two 1.41 +separate environments. See also ~~/src/Tools/SML/Examples.thy for 1.42 +some examples. 1.43 1.44 * More static checking of proof methods, which allows the system to 1.45 form a closure over the concrete syntax. Method arguments should be 1.46 @@ -37,25 +24,48 @@ 1.47 exception. Potential INCOMPATIBILITY for non-conformant tactical 1.48 proof tools. 1.49 1.50 -* Support for official Standard ML within the Isabelle context. 1.51 -Command 'SML_file' reads and evaluates the given Standard ML file. 1.52 -Toplevel bindings are stored within the theory context; the initial 1.53 -environment is restricted to the Standard ML implementation of 1.54 -Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' 1.55 -and 'SML_export' allow to exchange toplevel bindings between the two 1.56 -separate environments. See also ~~/src/Tools/SML/Examples.thy for 1.57 -some examples. 1.58 - 1.59 -* Updated and extended manuals: "codegen", "datatypes", 1.60 -"implementation", "jedit", "system". 1.61 +* Lexical syntax (inner and outer) supports text cartouches with 1.62 +arbitrary nesting, and without escapes of quotes etc. The Prover IDE 1.63 +supports input via ` (backquote). 1.64 + 1.65 +* The outer syntax categories "text" (for formal comments and document 1.66 +markup commands) and "altstring" (for literal fact references) allow 1.67 +cartouches as well, in addition to the traditional mix of quotations. 1.68 + 1.69 +* Syntax of document antiquotation @{rail} now uses \<newline> instead 1.70 +of "\\", to avoid the optical illusion of escaped backslash within 1.71 +string token. General renovation of its syntax using text cartouces. 1.72 +Minor INCOMPATIBILITY. 1.73 + 1.74 +* Discontinued legacy_isub_isup, which was a temporary workaround for 1.75 +Isabelle/ML in Isabelle2013-1. The prover process no longer accepts 1.76 +old identifier syntax with \<^isub> or \<^isup>. Potential 1.77 +INCOMPATIBILITY. 1.78 + 1.79 +* Document antiquotation @{url} produces markup for the given URL, 1.80 +which results in an active hyperlink within the text. 1.81 + 1.82 +* Document antiquotation @{file_unchecked} is like @{file}, but does 1.83 +not check existence within the file-system. 1.84 + 1.85 +* Updated and extended manuals: codegen, datatypes, implementation, 1.86 +isar-ref, jedit, system. 1.87 1.88 1.89 *** Prover IDE -- Isabelle/Scala/jEdit *** 1.90 1.91 -* Document panel: simplied interaction where every single mouse click 1.92 -(re)opens document via desktop environment or as jEdit buffer. 1.93 - 1.94 -* Support for Navigator plugin (with toolbar buttons). 1.95 +* Improved Document panel: simplied interaction where every single 1.96 +mouse click (re)opens document via desktop environment or as jEdit 1.97 +buffer. 1.98 + 1.99 +* Support for Navigator plugin (with toolbar buttons), with connection 1.100 +to PIDE hyperlinks. 1.101 + 1.102 +* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. 1.103 +Open text buffers take precedence over copies within the file-system. 1.104 + 1.105 +* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for 1.106 +auxiliary ML files. 1.107 1.108 * Improved syntactic and semantic completion mechanism, with simple 1.109 templates, completion language context, name-space completion, 1.110 @@ -72,12 +82,6 @@ 1.111 * Integrated spell-checker for document text, comments etc. with 1.112 completion popup and context-menu. 1.113 1.114 -* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. 1.115 -Open text buffers take precedence over copies within the file-system. 1.116 - 1.117 -* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for 1.118 -auxiliary ML files. 1.119 - 1.120 * More general "Query" panel supersedes "Find" panel, with GUI access 1.121 to commands 'find_theorems' and 'find_consts', as well as print 1.122 operations for the context. Minor incompatibility in keyboard 1.123 @@ -91,10 +95,6 @@ 1.124 process, without requiring old-fashioned command-line invocation of 1.125 "isabelle jedit -m MODE". 1.126 1.127 -* New Simplifier Trace panel provides an interactive view of the 1.128 -simplification process, enabled by the "simplifier_trace" attribute 1.129 -within the context. 1.130 - 1.131 * More support for remote files (e.g. http) using standard Java 1.132 networking operations instead of jEdit virtual file-systems. 1.133 1.134 @@ -105,6 +105,11 @@ 1.135 and window placement wrt. main editor view; optional menu item to 1.136 "Detach" a copy where this makes sense. 1.137 1.138 +* New Simplifier Trace panel provides an interactive view of the 1.139 +simplification process, enabled by the "simplifier_trace" attribute 1.140 +within the context. 1.141 + 1.142 + 1.143 1.144 *** Pure *** 1.145 1.146 @@ -139,12 +144,12 @@ 1.147 * Low-level type-class commands 'classes', 'classrel', 'arities' have 1.148 been discontinued to avoid the danger of non-trivial axiomatization 1.149 that is not immediately visible. INCOMPATIBILITY, use regular 1.150 -'instance' with proof. The required OFCLASS(...) theorem might be 1.151 -postulated via 'axiomatization' beforehand, or the proof finished 1.152 -trivially if the underlying class definition is made vacuous (without 1.153 -any assumptions). See also Isabelle/ML operations 1.154 -Axclass.axiomatize_class, Axclass.axiomatize_classrel, 1.155 -Axclass.axiomatize_arity. 1.156 +'instance' command with proof. The required OFCLASS(...) theorem 1.157 +might be postulated via 'axiomatization' beforehand, or the proof 1.158 +finished trivially if the underlying class definition is made vacuous 1.159 +(without any assumptions). See also Isabelle/ML operations 1.160 +Axclass.class_axiomatization, Axclass.classrel_axiomatization, 1.161 +Axclass.arity_axiomatization. 1.162 1.163 * Attributes "where" and "of" allow an optional context of local 1.164 variables ('for' declaration): these variables become schematic in the 1.165 @@ -167,10 +172,10 @@ 1.166 1.167 * Inner syntax token language allows regular quoted strings "..." 1.168 (only makes sense in practice, if outer syntax is delimited 1.169 -differently). 1.170 - 1.171 -* Code generator preprocessor: explicit control of simp tracing 1.172 -on a per-constant basis. See attribute "code_preproc". 1.173 +differently, e.g. via cartouches). 1.174 + 1.175 +* Code generator preprocessor: explicit control of simp tracing on a 1.176 +per-constant basis. See attribute "code_preproc". 1.177 1.178 * Command 'print_term_bindings' supersedes 'print_binds' for clarity, 1.179 but the latter is retained some time as Proof General legacy. 1.180 @@ -180,63 +185,68 @@ 1.181 1.182 * Qualified String.implode and String.explode. INCOMPATIBILITY. 1.183 1.184 -* Command and antiquotation ''value'' are hardcoded against nbe and 1.185 -ML now. Minor INCOMPATIBILITY. 1.186 - 1.187 -* Separate command ''approximate'' for approximative computation 1.188 -in Decision_Procs/Approximation. Minor INCOMPATIBILITY. 1.189 +* Command and antiquotation "value" are now hardcoded against nbe and 1.190 +ML. Minor INCOMPATIBILITY. 1.191 + 1.192 +* Separate command "approximate" for approximative computation in 1.193 +src/HOL/Decision_Procs/Approximation. Minor INCOMPATIBILITY. 1.194 1.195 * Adjustion of INF and SUP operations: 1.196 - * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. 1.197 - * Consolidated theorem names containing INFI and SUPR: have INF 1.198 - and SUP instead uniformly. 1.199 - * More aggressive normalization of expressions involving INF and Inf 1.200 - or SUP and Sup. 1.201 - * INF_image and SUP_image do not unfold composition. 1.202 - * Dropped facts INF_comp, SUP_comp. 1.203 - * Default congruence rules strong_INF_cong and strong_SUP_cong, 1.204 - with simplifier implication in premises. Generalize and replace 1.205 - former INT_cong, SUP_cong 1.206 + - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. 1.207 + - Consolidated theorem names containing INFI and SUPR: have INF and 1.208 + SUP instead uniformly. 1.209 + - More aggressive normalization of expressions involving INF and Inf 1.210 + or SUP and Sup. 1.211 + - INF_image and SUP_image do not unfold composition. 1.212 + - Dropped facts INF_comp, SUP_comp. 1.213 + - Default congruence rules strong_INF_cong and strong_SUP_cong, with 1.214 + simplifier implication in premises. Generalize and replace former 1.215 + INT_cong, SUP_cong 1.216 + 1.217 INCOMPATIBILITY. 1.218 1.219 * Swapped orientation of facts image_comp and vimage_comp: 1.220 + 1.221 image_compose ~> image_comp [symmetric] 1.222 image_comp ~> image_comp [symmetric] 1.223 vimage_compose ~> vimage_comp [symmetric] 1.224 vimage_comp ~> vimage_comp [symmetric] 1.225 - INCOMPATIBILITY. 1.226 - 1.227 -* Simplifier: Enhanced solver of preconditions of rewrite rules 1.228 - can now deal with conjunctions. 1.229 - For help with converting proofs, the old behaviour of the simplifier 1.230 - can be restored like this: declare/using [[simp_legacy_precond]] 1.231 - This configuration option will disappear again in the future. 1.232 + 1.233 +INCOMPATIBILITY. 1.234 + 1.235 +* Simplifier: Enhanced solver of preconditions of rewrite rules can 1.236 +now deal with conjunctions. For help with converting proofs, the old 1.237 +behaviour of the simplifier can be restored like this: declare/using 1.238 +[[simp_legacy_precond]]. This configuration option will disappear 1.239 +again in the future. INCOMPATIBILITY. 1.240 1.241 * HOL-Word: 1.242 - * Abandoned fact collection "word_arith_alts", which is a 1.243 - duplicate of "word_arith_wis". 1.244 - * Dropped first (duplicated) element in fact collections 1.245 - "sint_word_ariths", "word_arith_alts", "uint_word_ariths", 1.246 - "uint_word_arith_bintrs". 1.247 - 1.248 -* Code generator: enforce case of identifiers only for strict 1.249 -target language requirements. INCOMPATIBILITY. 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 +* Code generator: enforce case of identifiers only for strict target 1.257 +language requirements. INCOMPATIBILITY. 1.258 1.259 * Code generator: explicit proof contexts in many ML interfaces. 1.260 INCOMPATIBILITY. 1.261 1.262 -* Code generator: minimize exported identifiers by default. 1.263 -Minor INCOMPATIBILITY. 1.264 - 1.265 -* Code generation for SML and OCaml: dropped arcane "no_signatures" option. 1.266 -Minor INCOMPATIBILITY. 1.267 +* Code generator: minimize exported identifiers by default. Minor 1.268 +INCOMPATIBILITY. 1.269 + 1.270 +* Code generation for SML and OCaml: dropped arcane "no_signatures" 1.271 +option. Minor INCOMPATIBILITY. 1.272 1.273 * Simproc "finite_Collect" is no longer enabled by default, due to 1.274 spurious crashes and other surprises. Potential INCOMPATIBILITY. 1.275 1.276 -* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". 1.277 - The "bnf", "wrap_free_constructors", "datatype_new", "codatatype", 1.278 - "primcorec", and "primcorecursive" commands are now part of "Main". 1.279 +* Moved new (co)datatype package and its dependencies from session 1.280 + "HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', 1.281 + 'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now 1.282 + part of theory "Main". 1.283 + 1.284 Theory renamings: 1.285 FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) 1.286 Library/Wfrec.thy ~> Wfrec.thy 1.287 @@ -260,58 +270,63 @@ 1.288 BNF/More_BNFs.thy ~> Library/More_BNFs.thy 1.289 BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy 1.290 BNF/Examples/* ~> BNF_Examples/* 1.291 + 1.292 New theories: 1.293 Wellorder_Extension.thy (split from Zorn.thy) 1.294 Library/Cardinal_Notations.thy 1.295 Library/BNF_Axomatization.thy 1.296 BNF_Examples/Misc_Primcorec.thy 1.297 BNF_Examples/Stream_Processor.thy 1.298 + 1.299 Discontinued theories: 1.300 BNF/BNF.thy 1.301 BNF/Equiv_Relations_More.thy 1.302 - INCOMPATIBILITY. 1.303 + 1.304 +INCOMPATIBILITY. 1.305 1.306 * New (co)datatype package: 1.307 - * "primcorec" is fully implemented. 1.308 - * "datatype_new" generates size functions ("size_xxx" and "size") as 1.309 - required by "fun". 1.310 - * BNFs are integrated with the Lifting tool and new-style (co)datatypes 1.311 - with Transfer. 1.312 - * Renamed commands: 1.313 + - Command 'primcorec' is fully implemented. 1.314 + - Command 'datatype_new' generates size functions ("size_xxx" and 1.315 + "size") as required by 'fun'. 1.316 + - BNFs are integrated with the Lifting tool and new-style 1.317 + (co)datatypes with Transfer. 1.318 + - Renamed commands: 1.319 datatype_new_compat ~> datatype_compat 1.320 primrec_new ~> primrec 1.321 wrap_free_constructors ~> free_constructors 1.322 INCOMPATIBILITY. 1.323 - * The generated constants "xxx_case" and "xxx_rec" have been renamed 1.324 + - The generated constants "xxx_case" and "xxx_rec" have been renamed 1.325 "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). 1.326 INCOMPATIBILITY. 1.327 - * The constant "xxx_(un)fold" and related theorems are no longer generated. 1.328 - Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec". 1.329 + - The constant "xxx_(un)fold" and related theorems are no longer 1.330 + generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually 1.331 + using "prim(co)rec". 1.332 INCOMPATIBILITY. 1.333 - * No discriminators are generated for nullary constructors by default, 1.334 - eliminating the need for the odd "=:" syntax. 1.335 + - No discriminators are generated for nullary constructors by 1.336 + default, eliminating the need for the odd "=:" syntax. 1.337 INCOMPATIBILITY. 1.338 - * No discriminators or selectors are generated by default by 1.339 + - No discriminators or selectors are generated by default by 1.340 "datatype_new", unless custom names are specified or the new 1.341 "discs_sels" option is passed. 1.342 INCOMPATIBILITY. 1.343 1.344 * Old datatype package: 1.345 - * The generated theorems "xxx.cases" and "xxx.recs" have been renamed 1.346 - "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case"). 1.347 - INCOMPATIBILITY. 1.348 - * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been 1.349 - renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~> 1.350 - "case_prod"). 1.351 - INCOMPATIBILITY. 1.352 - 1.353 -* The types "'a list" and "'a option", their set and map functions, their 1.354 - relators, and their selectors are now produced using the new BNF-based 1.355 - datatype package. 1.356 + - The generated theorems "xxx.cases" and "xxx.recs" have been 1.357 + renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> 1.358 + "sum.case"). INCOMPATIBILITY. 1.359 + - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have 1.360 + been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., 1.361 + "prod_case" ~> "case_prod"). INCOMPATIBILITY. 1.362 + 1.363 +* The types "'a list" and "'a option", their set and map functions, 1.364 + their relators, and their selectors are now produced using the new 1.365 + BNF-based datatype package. 1.366 + 1.367 Renamed constants: 1.368 Option.set ~> set_option 1.369 Option.map ~> map_option 1.370 option_rel ~> rel_option 1.371 + 1.372 Renamed theorems: 1.373 set_def ~> set_rec[abs_def] 1.374 map_def ~> map_rec[abs_def] 1.375 @@ -323,7 +338,8 @@ 1.376 hd.simps ~> list.sel(1) 1.377 tl.simps ~> list.sel(2-3) 1.378 the.simps ~> option.sel 1.379 - INCOMPATIBILITY. 1.380 + 1.381 +INCOMPATIBILITY. 1.382 1.383 * The following map functions and relators have been renamed: 1.384 sum_map ~> map_sum 1.385 @@ -333,16 +349,18 @@ 1.386 fun_rel ~> rel_fun 1.387 set_rel ~> rel_set 1.388 filter_rel ~> rel_filter 1.389 - fset_rel ~> rel_fset (in "Library/FSet.thy") 1.390 - cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy") 1.391 - vset ~> rel_vset (in "Library/Quotient_Set.thy") 1.392 - 1.393 -* New theories: 1.394 - Cardinals/Ordinal_Arithmetic.thy 1.395 - Library/Tree 1.396 - 1.397 -* Theory reorganizations: 1.398 - * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy 1.399 + fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy") 1.400 + cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy") 1.401 + vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy") 1.402 + 1.403 +INCOMPATIBILITY. 1.404 + 1.405 +* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. 1.406 + 1.407 +* New theory src/HOL/Library/Tree.thy. 1.408 + 1.409 +* Theory reorganization: 1.410 + Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy 1.411 1.412 * Consolidated some facts about big group operators: 1.413 1.414 @@ -411,41 +429,41 @@ 1.415 Dropped setsum_reindex_id, setprod_reindex_id 1.416 (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]). 1.417 1.418 - INCOMPATIBILITY. 1.419 - 1.420 -* New internal SAT solver "cdclite" that produces models and proof traces. 1.421 - This solver replaces the internal SAT solvers "enumerate" and "dpll". 1.422 - Applications that explicitly used one of these two SAT solvers should 1.423 - use "cdclite" instead. In addition, "cdclite" is now the default SAT 1.424 - solver for the "sat" and "satx" proof methods and corresponding tactics; 1.425 - the old default can be restored using 1.426 - "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. 1.427 - 1.428 -* SMT module: 1.429 - * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 1.430 - and supports recent versions of Z3 (e.g., 4.3). The new proof method is 1.431 - called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no 1.432 - longer supported, because no version of the solver can handle both 1.433 - SMT-LIB 2 and quantifiers. 1.434 +INCOMPATIBILITY. 1.435 + 1.436 +* New internal SAT solver "cdclite" that produces models and proof 1.437 +traces. This solver replaces the internal SAT solvers "enumerate" and 1.438 +"dpll". Applications that explicitly used one of these two SAT 1.439 +solvers should use "cdclite" instead. In addition, "cdclite" is now 1.440 +the default SAT solver for the "sat" and "satx" proof methods and 1.441 +corresponding tactics; the old default can be restored using "declare 1.442 +[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. 1.443 + 1.444 +* SMT module: A new version of the SMT module, temporarily called 1.445 +"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 1.446 +4.3). The new proof method is called "smt2". CVC3 and CVC4 are also 1.447 +supported as oracles. Yices is no longer supported, because no version 1.448 +of the solver can handle both SMT-LIB 2 and quantifiers. 1.449 1.450 * Sledgehammer: 1.451 - Z3 can now produce Isar proofs. 1.452 - MaSh overhaul: 1.453 - - New SML-based learning engines eliminate the dependency on Python 1.454 - and increase performance and reliability. 1.455 - - MaSh and MeSh are now used by default together with the traditional 1.456 - MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh" 1.457 - system option in Plugin Options / Isabelle / General to "none". 1.458 + . New SML-based learning engines eliminate the dependency on 1.459 + Python and increase performance and reliability. 1.460 + . MaSh and MeSh are now used by default together with the 1.461 + traditional MePo (Meng-Paulson) relevance filter. To disable 1.462 + MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin 1.463 + Options / Isabelle / General to "none". 1.464 - New option: 1.465 smt_proofs 1.466 - Renamed options: 1.467 isar_compress ~> compress 1.468 isar_try0 ~> try0 1.469 - INCOMPATIBILITY. 1.470 - 1.471 -* Metis: 1.472 - - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead. 1.473 - INCOMPATIBILITY. 1.474 + 1.475 +INCOMPATIBILITY. 1.476 + 1.477 +* Metis: Removed legacy proof method 'metisFT'. Use 'metis 1.478 +(full_types)' instead. INCOMPATIBILITY. 1.479 1.480 * Try0: Added 'algebra' and 'meson' to the set of proof methods. 1.481 1.482 @@ -467,7 +485,7 @@ 1.483 1.484 * Abolished slightly odd global lattice interpretation for min/max. 1.485 1.486 -Fact consolidations: 1.487 + Fact consolidations: 1.488 min_max.inf_assoc ~> min.assoc 1.489 min_max.inf_commute ~> min.commute 1.490 min_max.inf_left_commute ~> min.left_commute 1.491 @@ -513,18 +531,18 @@ 1.492 min.left_commute, min.left_idem, max.commute, max.assoc, 1.493 max.left_commute, max.left_idem directly. 1.494 1.495 -For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2, 1.496 -max.cobounded1m max.cobounded2 directly. 1.497 +For min_max.inf_sup_ord, prefer (one of) min.cobounded1, 1.498 +min.cobounded2, max.cobounded1m max.cobounded2 directly. 1.499 1.500 For min_ac or max_ac, prefer more general collection ac_simps. 1.501 1.502 INCOMPATBILITY. 1.503 1.504 -* Word library: bit representations prefer type bool over type bit. 1.505 -INCOMPATIBILITY. 1.506 - 1.507 -* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin. 1.508 -INCOMPATIBILITY. 1.509 +* HOL-Word: bit representations prefer type bool over type bit. 1.510 +INCOMPATIBILITY. 1.511 + 1.512 +* Theorem disambiguation Inf_le_Sup (on finite sets) ~> 1.513 +Inf_fin_le_Sup_fin. INCOMPATIBILITY. 1.514 1.515 * Code generations are provided for make, fields, extend and truncate 1.516 operations on records. 1.517 @@ -534,21 +552,25 @@ 1.518 1.519 * Fact generalization and consolidation: 1.520 neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 1.521 -INCOMPATIBILITY. 1.522 - 1.523 -* Purely algebraic definition of even. Fact generalization and consolidation: 1.524 + 1.525 +INCOMPATIBILITY. 1.526 + 1.527 +* Purely algebraic definition of even. Fact generalization and 1.528 + consolidation: 1.529 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd 1.530 even_zero_(nat|int) ~> even_zero 1.531 + 1.532 INCOMPATIBILITY. 1.533 1.534 * Abolished neg_numeral. 1.535 - * Canonical representation for minus one is "- 1". 1.536 - * Canonical representation for other negative numbers is "- (numeral _)". 1.537 - * When devising rule sets for number calculation, consider the 1.538 + - Canonical representation for minus one is "- 1". 1.539 + - Canonical representation for other negative numbers is "- (numeral _)". 1.540 + - When devising rule sets for number calculation, consider the 1.541 following canonical cases: 0, 1, numeral _, - 1, - numeral _. 1.542 - * HOLogic.dest_number also recognizes numerals in non-canonical forms 1.543 + - HOLogic.dest_number also recognizes numerals in non-canonical forms 1.544 like "numeral One", "- numeral One", "- 0" and even "- ... - _". 1.545 - * Syntax for negative numerals is mere input syntax. 1.546 + - Syntax for negative numerals is mere input syntax. 1.547 + 1.548 INCOMPATIBILITY. 1.549 1.550 * Elimination of fact duplicates: 1.551 @@ -556,6 +578,7 @@ 1.552 diff_eq_0_iff_eq ~> right_minus_eq 1.553 nat_infinite ~> infinite_UNIV_nat 1.554 int_infinite ~> infinite_UNIV_int 1.555 + 1.556 INCOMPATIBILITY. 1.557 1.558 * Fact name consolidation: 1.559 @@ -564,6 +587,7 @@ 1.560 le_minus_self_iff ~> less_eq_neg_nonpos 1.561 neg_less_nonneg ~> neg_less_pos 1.562 less_minus_self_iff ~> less_neg_neg [simp] 1.563 + 1.564 INCOMPATIBILITY. 1.565 1.566 * More simplification rules on unary and binary minus: 1.567 @@ -571,9 +595,9 @@ 1.568 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, 1.569 add_minus_cancel, diff_add_cancel, le_add_same_cancel1, 1.570 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, 1.571 -minus_add_cancel, uminus_add_conv_diff. These correspondingly 1.572 -have been taken away from fact collections algebra_simps and 1.573 -field_simps. INCOMPATIBILITY. 1.574 +minus_add_cancel, uminus_add_conv_diff. These correspondingly have 1.575 +been taken away from fact collections algebra_simps and field_simps. 1.576 +INCOMPATIBILITY. 1.577 1.578 To restore proofs, the following patterns are helpful: 1.579 1.580 @@ -588,18 +612,18 @@ 1.581 or the brute way with 1.582 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". 1.583 1.584 -* SUP and INF generalized to conditionally_complete_lattice 1.585 +* SUP and INF generalized to conditionally_complete_lattice. 1.586 1.587 * Theory Lubs moved HOL image to HOL-Library. It is replaced by 1.588 -Conditionally_Complete_Lattices. INCOMPATIBILITY. 1.589 - 1.590 -* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them 1.591 -instead of explicitly stating boundedness of sets. 1.592 - 1.593 -* ccpo.admissible quantifies only over non-empty chains to allow 1.594 -more syntax-directed proof rules; the case of the empty chain 1.595 -shows up as additional case in fixpoint induction proofs. 1.596 -INCOMPATIBILITY 1.597 +Conditionally_Complete_Lattices. INCOMPATIBILITY. 1.598 + 1.599 +* Introduce bdd_above and bdd_below in theory 1.600 +Conditionally_Complete_Lattices, use them instead of explicitly 1.601 +stating boundedness of sets. 1.602 + 1.603 +* ccpo.admissible quantifies only over non-empty chains to allow more 1.604 +syntax-directed proof rules; the case of the empty chain shows up as 1.605 +additional case in fixpoint induction proofs. INCOMPATIBILITY. 1.606 1.607 * Removed and renamed theorems in Series: 1.608 summable_le ~> suminf_le 1.609 @@ -617,10 +641,13 @@ 1.610 removed series_zero, replaced by sums_finite 1.611 1.612 removed auxiliary lemmas: 1.613 + 1.614 sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group, 1.615 - half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded, 1.616 - summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom, 1.617 - sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const 1.618 + half, le_Suc_ex_iff, lemma_realpow_diff_sumr, 1.619 + real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2, 1.620 + sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero, 1.621 + summable_convergent_sumr_iff, sumr_diff_mult_const 1.622 + 1.623 INCOMPATIBILITY. 1.624 1.625 * Replace (F)DERIV syntax by has_derivative: 1.626 @@ -632,10 +659,10 @@ 1.627 1.628 - removed constant isDiff 1.629 1.630 - - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input 1.631 - syntax. 1.632 - 1.633 - - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed 1.634 + - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as 1.635 + input syntax. 1.636 + 1.637 + - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed. 1.638 1.639 - Renamed FDERIV_... lemmas to has_derivative_... 1.640 1.641 @@ -643,8 +670,9 @@ 1.642 1.643 - removed DERIV_intros, has_derivative_eq_intros 1.644 1.645 - - introduced derivative_intros and deriative_eq_intros which includes now rules for 1.646 - DERIV, has_derivative and has_vector_derivative. 1.647 + - introduced derivative_intros and deriative_eq_intros which 1.648 + includes now rules for DERIV, has_derivative and 1.649 + has_vector_derivative. 1.650 1.651 - Other renamings: 1.652 differentiable_def ~> real_differentiable_def 1.653 @@ -654,24 +682,27 @@ 1.654 isDiff_der ~> differentiable_def 1.655 deriv_fderiv ~> has_field_derivative_def 1.656 deriv_def ~> DERIV_def 1.657 -INCOMPATIBILITY. 1.658 - 1.659 -* Include more theorems in continuous_intros. Remove the continuous_on_intros, 1.660 - isCont_intros collections, these facts are now in continuous_intros. 1.661 - 1.662 -* Theorems about complex numbers are now stated only using Re and Im, the Complex 1.663 - constructor is not used anymore. It is possible to use primcorec to defined the 1.664 - behaviour of a complex-valued function. 1.665 - 1.666 - Removed theorems about the Complex constructor from the simpset, they are 1.667 - available as the lemma collection legacy_Complex_simps. This especially 1.668 - removes 1.669 + 1.670 +INCOMPATIBILITY. 1.671 + 1.672 +* Include more theorems in continuous_intros. Remove the 1.673 +continuous_on_intros, isCont_intros collections, these facts are now 1.674 +in continuous_intros. 1.675 + 1.676 +* Theorems about complex numbers are now stated only using Re and Im, 1.677 +the Complex constructor is not used anymore. It is possible to use 1.678 +primcorec to defined the behaviour of a complex-valued function. 1.679 + 1.680 +Removed theorems about the Complex constructor from the simpset, they 1.681 +are available as the lemma collection legacy_Complex_simps. This 1.682 +especially removes 1.683 + 1.684 i_complex_of_real: "ii * complex_of_real r = Complex 0 r". 1.685 1.686 - Instead the reverse direction is supported with 1.687 +Instead the reverse direction is supported with 1.688 Complex_eq: "Complex a b = a + \<i> * b" 1.689 1.690 - Moved csqrt from Fundamental_Algebra_Theorem to Complex. 1.691 +Moved csqrt from Fundamental_Algebra_Theorem to Complex. 1.692 1.693 Renamings: 1.694 Re/Im ~> complex.sel 1.695 @@ -701,36 +732,37 @@ 1.696 complex_inverse_def 1.697 complex_scaleR_def 1.698 1.699 +INCOMPATIBILITY. 1.700 + 1.701 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. 1.702 1.703 * Nitpick: 1.704 - - Fixed soundness bug whereby mutually recursive datatypes could take 1.705 - infinite values. 1.706 - - Fixed soundness bug with low-level number functions such as "Abs_Integ" and 1.707 - "Rep_Integ". 1.708 + - Fixed soundness bug whereby mutually recursive datatypes could 1.709 + take infinite values. 1.710 + - Fixed soundness bug with low-level number functions such as 1.711 + "Abs_Integ" and "Rep_Integ". 1.712 - Removed "std" option. 1.713 - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to 1.714 "hide_types". 1.715 1.716 * HOL-Multivariate_Analysis: 1.717 - - type class ordered_real_vector for ordered vector spaces 1.718 - - new theory Complex_Basic_Analysis defining complex derivatives, 1.719 + - Type class ordered_real_vector for ordered vector spaces. 1.720 + - New theory Complex_Basic_Analysis defining complex derivatives, 1.721 holomorphic functions, etc., ported from HOL Light's canal.ml. 1.722 - - changed order of ordered_euclidean_space to be compatible with 1.723 + - Changed order of ordered_euclidean_space to be compatible with 1.724 pointwise ordering on products. Therefore instance of 1.725 conditionally_complete_lattice and ordered_real_vector. 1.726 INCOMPATIBILITY: use box instead of greaterThanLessThan or 1.727 - explicit set-comprehensions with eucl_less for other (half-) open 1.728 + explicit set-comprehensions with eucl_less for other (half-)open 1.729 intervals. 1.730 - 1.731 - renamed theorems: 1.732 derivative_linear ~> has_derivative_bounded_linear 1.733 derivative_is_linear ~> has_derivative_linear 1.734 bounded_linear_imp_linear ~> bounded_linear.linear 1.735 1.736 * HOL-Probability: 1.737 - - replaced the Lebesgue integral on real numbers by the more general Bochner 1.738 - integral for functions into a real-normed vector space. 1.739 + - replaced the Lebesgue integral on real numbers by the more general 1.740 + Bochner integral for functions into a real-normed vector space. 1.741 1.742 integral_zero ~> integral_zero / integrable_zero 1.743 integral_minus ~> integral_minus / integrable_minus 1.744 @@ -793,15 +825,17 @@ 1.745 1.746 - Renamed positive_integral to nn_integral: 1.747 1.748 - * Renamed all lemmas "*positive_integral*" to *nn_integral*" 1.749 + . Renamed all lemmas "*positive_integral*" to *nn_integral*" 1.750 positive_integral_positive ~> nn_integral_nonneg 1.751 1.752 - * Renamed abbreviation integral\<^sup>P to integral\<^sup>N. 1.753 - 1.754 - - Formalized properties about exponentially, Erlang, and normal distributed 1.755 - random variables. 1.756 - 1.757 -* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it. 1.758 + . Renamed abbreviation integral\<^sup>P to integral\<^sup>N. 1.759 + 1.760 + - Formalized properties about exponentially, Erlang, and normal 1.761 + distributed random variables. 1.762 + 1.763 +* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by 1.764 +session Kleene_Algebra in AFP. 1.765 + 1.766 1.767 *** Scala *** 1.768 1.769 @@ -811,6 +845,9 @@ 1.770 specific and may override results accumulated so far. The elements 1.771 guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. 1.772 1.773 +* Substantial reworking of internal PIDE protocol communication 1.774 +channels. INCOMPATIBILITY. 1.775 + 1.776 1.777 *** ML *** 1.778 1.779 @@ -818,8 +855,8 @@ 1.780 structure Runtime. Minor INCOMPATIBILITY. 1.781 1.782 * Discontinued old Toplevel.debug in favour of system option 1.783 -"ML_exception_trace", which may be also declared within the context via 1.784 -"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. 1.785 +"ML_exception_trace", which may be also declared within the context 1.786 +via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. 1.787 1.788 * Renamed configuration option "ML_trace" to "ML_source_trace". Minor 1.789 INCOMPATIBILITY. 1.790 @@ -878,21 +915,6 @@ 1.791 the "system" manual for general explanations about add-on components, 1.792 notably those that are not bundled with the normal release. 1.793 1.794 -* Session ROOT specifications require explicit 'document_files' for 1.795 -robust dependencies on LaTeX sources. Only these explicitly given 1.796 -files are copied to the document output directory, before document 1.797 -processing is started. 1.798 - 1.799 -* Simplified "isabelle display" tool. Settings variables DVI_VIEWER 1.800 -and PDF_VIEWER now refer to the actual programs, not shell 1.801 -command-lines. Discontinued option -c: invocation may be asynchronous 1.802 -via desktop environment, without any special precautions. Potential 1.803 -INCOMPATIBILITY with ambitious private settings. 1.804 - 1.805 -* Improved 'display_drafts' concerning desktop integration and 1.806 -repeated invocation in PIDE front-end: re-use single file 1.807 -$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. 1.808 - 1.809 * The raw Isabelle process executable has been renamed from 1.810 "isabelle-process" to "isabelle_process", which conforms to common 1.811 shell naming conventions, and allows to define a shell function within 1.812 @@ -904,16 +926,31 @@ 1.813 with implicit build like "isabelle jedit", and without the mostly 1.814 obsolete Isar TTY loop. 1.815 1.816 +* Simplified "isabelle display" tool. Settings variables DVI_VIEWER 1.817 +and PDF_VIEWER now refer to the actual programs, not shell 1.818 +command-lines. Discontinued option -c: invocation may be asynchronous 1.819 +via desktop environment, without any special precautions. Potential 1.820 +INCOMPATIBILITY with ambitious private settings. 1.821 + 1.822 * Removed obsolete "isabelle unsymbolize". Note that the usual format 1.823 for email communication is the Unicode rendering of Isabelle symbols, 1.824 as produced by Isabelle/jEdit, for example. 1.825 1.826 -* Retired the now unused Isabelle tool "wwwfind". Similar 1.827 -functionality may be integrated into PIDE/jEdit at a later point. 1.828 +* Removed obsolete tool "wwwfind". Similar functionality may be 1.829 +integrated into Isabelle/jEdit eventually. 1.830 + 1.831 +* Improved 'display_drafts' concerning desktop integration and 1.832 +repeated invocation in PIDE front-end: re-use single file 1.833 +$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. 1.834 1.835 * Windows: support for regular TeX installation (e.g. MiKTeX) instead 1.836 of TeX Live from Cygwin. 1.837 1.838 +* Session ROOT specifications require explicit 'document_files' for 1.839 +robust dependencies on LaTeX sources. Only these explicitly given 1.840 +files are copied to the document output directory, before document 1.841 +processing is started. 1.842 + 1.843 1.844 1.845 New in Isabelle2013-2 (December 2013)