author | wenzelm |

Fri Jul 04 16:50:57 2014 +0200 (2014-07-04) | |

changeset 57508 | 19240ff4b02d |

parent 57507 | a609065c9e15 |

child 57509 | cca0db87b653 |

misc tuning for release;

1.1 --- a/NEWS Fri Jul 04 15:50:28 2014 +0200 1.2 +++ b/NEWS Fri Jul 04 16:50:57 2014 +0200 1.3 @@ -223,29 +223,6 @@ 1.4 1.5 * Qualified String.implode and String.explode. INCOMPATIBILITY. 1.6 1.7 -* Adjustion of INF and SUP operations: 1.8 - - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. 1.9 - - Consolidated theorem names containing INFI and SUPR: have INF and 1.10 - SUP instead uniformly. 1.11 - - More aggressive normalization of expressions involving INF and Inf 1.12 - or SUP and Sup. 1.13 - - INF_image and SUP_image do not unfold composition. 1.14 - - Dropped facts INF_comp, SUP_comp. 1.15 - - Default congruence rules strong_INF_cong and strong_SUP_cong, with 1.16 - simplifier implication in premises. Generalize and replace former 1.17 - INT_cong, SUP_cong 1.18 - 1.19 -INCOMPATIBILITY. 1.20 - 1.21 -* Swapped orientation of facts image_comp and vimage_comp: 1.22 - 1.23 - image_compose ~> image_comp [symmetric] 1.24 - image_comp ~> image_comp [symmetric] 1.25 - vimage_compose ~> vimage_comp [symmetric] 1.26 - vimage_comp ~> vimage_comp [symmetric] 1.27 - 1.28 -INCOMPATIBILITY. 1.29 - 1.30 * Simplifier: Enhanced solver of preconditions of rewrite rules can 1.31 now deal with conjunctions. For help with converting proofs, the old 1.32 behaviour of the simplifier can be restored like this: declare/using 1.33 @@ -368,6 +345,83 @@ 1.34 1.35 INCOMPATIBILITY. 1.36 1.37 +* New internal SAT solver "cdclite" that produces models and proof 1.38 +traces. This solver replaces the internal SAT solvers "enumerate" and 1.39 +"dpll". Applications that explicitly used one of these two SAT 1.40 +solvers should use "cdclite" instead. In addition, "cdclite" is now 1.41 +the default SAT solver for the "sat" and "satx" proof methods and 1.42 +corresponding tactics; the old default can be restored using "declare 1.43 +[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. 1.44 + 1.45 +* SMT module: A new version of the SMT module, temporarily called 1.46 +"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 1.47 +4.3). The new proof method is called "smt2". CVC3 and CVC4 are also 1.48 +supported as oracles. Yices is no longer supported, because no version 1.49 +of the solver can handle both SMT-LIB 2 and quantifiers. 1.50 + 1.51 +* Activation of Z3 now works via "z3_non_commercial" system option 1.52 +(without requiring restart), instead of former settings variable 1.53 +"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu 1.54 +Plugin Options / Isabelle / General. 1.55 + 1.56 +* Sledgehammer: 1.57 + - Z3 can now produce Isar proofs. 1.58 + - MaSh overhaul: 1.59 + . New SML-based learning engines eliminate the dependency on 1.60 + Python and increase performance and reliability. 1.61 + . MaSh and MeSh are now used by default together with the 1.62 + traditional MePo (Meng-Paulson) relevance filter. To disable 1.63 + MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin 1.64 + Options / Isabelle / General to "none". 1.65 + - New option: 1.66 + smt_proofs 1.67 + - Renamed options: 1.68 + isar_compress ~> compress 1.69 + isar_try0 ~> try0 1.70 + 1.71 +INCOMPATIBILITY. 1.72 + 1.73 +* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. 1.74 + 1.75 +* Nitpick: 1.76 + - Fixed soundness bug whereby mutually recursive datatypes could 1.77 + take infinite values. 1.78 + - Fixed soundness bug with low-level number functions such as 1.79 + "Abs_Integ" and "Rep_Integ". 1.80 + - Removed "std" option. 1.81 + - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to 1.82 + "hide_types". 1.83 + 1.84 +* Metis: Removed legacy proof method 'metisFT'. Use 'metis 1.85 +(full_types)' instead. INCOMPATIBILITY. 1.86 + 1.87 +* Try0: Added 'algebra' and 'meson' to the set of proof methods. 1.88 + 1.89 +* Adjustion of INF and SUP operations: 1.90 + - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. 1.91 + - Consolidated theorem names containing INFI and SUPR: have INF and 1.92 + SUP instead uniformly. 1.93 + - More aggressive normalization of expressions involving INF and Inf 1.94 + or SUP and Sup. 1.95 + - INF_image and SUP_image do not unfold composition. 1.96 + - Dropped facts INF_comp, SUP_comp. 1.97 + - Default congruence rules strong_INF_cong and strong_SUP_cong, with 1.98 + simplifier implication in premises. Generalize and replace former 1.99 + INT_cong, SUP_cong 1.100 + 1.101 +INCOMPATIBILITY. 1.102 + 1.103 +* SUP and INF generalized to conditionally_complete_lattice. 1.104 + 1.105 +* Swapped orientation of facts image_comp and vimage_comp: 1.106 + 1.107 + image_compose ~> image_comp [symmetric] 1.108 + image_comp ~> image_comp [symmetric] 1.109 + vimage_compose ~> vimage_comp [symmetric] 1.110 + vimage_comp ~> vimage_comp [symmetric] 1.111 + 1.112 +INCOMPATIBILITY. 1.113 + 1.114 * Theory reorganization: split of Big_Operators.thy into 1.115 Groups_Big.thy and Lattices_Big.thy. 1.116 1.117 @@ -440,47 +494,6 @@ 1.118 1.119 INCOMPATIBILITY. 1.120 1.121 -* New internal SAT solver "cdclite" that produces models and proof 1.122 -traces. This solver replaces the internal SAT solvers "enumerate" and 1.123 -"dpll". Applications that explicitly used one of these two SAT 1.124 -solvers should use "cdclite" instead. In addition, "cdclite" is now 1.125 -the default SAT solver for the "sat" and "satx" proof methods and 1.126 -corresponding tactics; the old default can be restored using "declare 1.127 -[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. 1.128 - 1.129 -* SMT module: A new version of the SMT module, temporarily called 1.130 -"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 1.131 -4.3). The new proof method is called "smt2". CVC3 and CVC4 are also 1.132 -supported as oracles. Yices is no longer supported, because no version 1.133 -of the solver can handle both SMT-LIB 2 and quantifiers. 1.134 - 1.135 -* Sledgehammer: 1.136 - - Z3 can now produce Isar proofs. 1.137 - - MaSh overhaul: 1.138 - . New SML-based learning engines eliminate the dependency on 1.139 - Python and increase performance and reliability. 1.140 - . MaSh and MeSh are now used by default together with the 1.141 - traditional MePo (Meng-Paulson) relevance filter. To disable 1.142 - MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin 1.143 - Options / Isabelle / General to "none". 1.144 - - New option: 1.145 - smt_proofs 1.146 - - Renamed options: 1.147 - isar_compress ~> compress 1.148 - isar_try0 ~> try0 1.149 - 1.150 -INCOMPATIBILITY. 1.151 - 1.152 -* Metis: Removed legacy proof method 'metisFT'. Use 'metis 1.153 -(full_types)' instead. INCOMPATIBILITY. 1.154 - 1.155 -* Try0: Added 'algebra' and 'meson' to the set of proof methods. 1.156 - 1.157 -* Activation of Z3 now works via "z3_non_commercial" system option 1.158 -(without requiring restart), instead of former settings variable 1.159 -"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu 1.160 -Plugin Options / Isabelle / General. 1.161 - 1.162 * Abolished slightly odd global lattice interpretation for min/max. 1.163 1.164 Fact consolidations: 1.165 @@ -604,8 +617,6 @@ 1.166 or the brute way with 1.167 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". 1.168 1.169 -* SUP and INF generalized to conditionally_complete_lattice. 1.170 - 1.171 * Introduce bdd_above and bdd_below in theory 1.172 Conditionally_Complete_Lattices, use them instead of explicitly 1.173 stating boundedness of sets. 1.174 @@ -723,17 +734,6 @@ 1.175 1.176 INCOMPATIBILITY. 1.177 1.178 -* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. 1.179 - 1.180 -* Nitpick: 1.181 - - Fixed soundness bug whereby mutually recursive datatypes could 1.182 - take infinite values. 1.183 - - Fixed soundness bug with low-level number functions such as 1.184 - "Abs_Integ" and "Rep_Integ". 1.185 - - Removed "std" option. 1.186 - - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to 1.187 - "hide_types". 1.188 - 1.189 * Theory Lubs moved HOL image to HOL-Library. It is replaced by 1.190 Conditionally_Complete_Lattices. INCOMPATIBILITY. 1.191