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