document latest changes to Meson/Metis/Sledgehammer
authorblanchet
Tue Oct 05 12:06:08 2010 +0200 (2010-10-05)
changeset 399572f2d90cc31a2
parent 39956 132b79985660
child 39958 88c9aa5666de
document latest changes to Meson/Metis/Sledgehammer
NEWS
     1.1 --- a/NEWS	Tue Oct 05 12:04:57 2010 +0200
     1.2 +++ b/NEWS	Tue Oct 05 12:06:08 2010 +0200
     1.3 @@ -244,6 +244,46 @@
     1.4  * Function package: .psimps rules are no longer implicitly declared [simp].
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Weaker versions of the "meson" and "metis" proof methods are now available in
     1.8 +  "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become
     1.9 +  more powerful after "Hilbert_Choice" is loaded in "HOL-Main".
    1.10 +
    1.11 +* MESON: Renamed lemmas:
    1.12 +  meson_not_conjD ~> Meson.not_conjD
    1.13 +  meson_not_disjD ~> Meson.not_disjD
    1.14 +  meson_not_notD ~> Meson.not_notD
    1.15 +  meson_not_allD ~> Meson.not_allD
    1.16 +  meson_not_exD ~> Meson.not_exD
    1.17 +  meson_imp_to_disjD ~> Meson.imp_to_disjD
    1.18 +  meson_not_impD ~> Meson.not_impD
    1.19 +  meson_iff_to_disjD ~> Meson.iff_to_disjD
    1.20 +  meson_not_iffD ~> Meson.not_iffD
    1.21 +  meson_not_refl_disj_D ~> Meson.not_refl_disj_D
    1.22 +  meson_conj_exD1 ~> Meson.conj_exD1
    1.23 +  meson_conj_exD2 ~> Meson.conj_exD2
    1.24 +  meson_disj_exD ~> Meson.disj_exD
    1.25 +  meson_disj_exD1 ~> Meson.disj_exD1
    1.26 +  meson_disj_exD2 ~> Meson.disj_exD2
    1.27 +  meson_disj_assoc ~> Meson.disj_assoc
    1.28 +  meson_disj_comm ~> Meson.disj_comm
    1.29 +  meson_disj_FalseD1 ~> Meson.disj_FalseD1
    1.30 +  meson_disj_FalseD2 ~> Meson.disj_FalseD2
    1.31 +INCOMPATIBILITY.
    1.32 +
    1.33 +* Sledgehammer: Renamed lemmas:
    1.34 +  COMBI_def ~> Meson.COMBI_def
    1.35 +  COMBK_def ~> Meson.COMBK_def
    1.36 +  COMBB_def ~> Meson.COMBB_def
    1.37 +  COMBC_def ~> Meson.COMBC_def
    1.38 +  COMBS_def ~> Meson.COMBS_def
    1.39 +  abs_I ~> Meson.abs_I
    1.40 +  abs_K ~> Meson.abs_K
    1.41 +  abs_B ~> Meson.abs_B
    1.42 +  abs_C ~> Meson.abs_C
    1.43 +  abs_S ~> Meson.abs_S
    1.44 +INCOMPATIBILITY.
    1.45 +
    1.46 +
    1.47  *** FOL ***
    1.48  
    1.49  * All constant names are now qualified.  INCOMPATIBILITY.