NEWS
changeset 57508 19240ff4b02d
parent 57504 5cf245c62c4c
child 57512 cc97b347b301
     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