[isabelle-dev] NEWS

[Jasmin Christian Blanchette]

* Old and new SMT modules:
  - The old 'smt' method has been renamed 'old_smt' and moved to
    'src/HOL/Library/Old_SMT.thy'. It provided for compatibility, until
    applications have been ported to use the new 'smt' method. For the
    method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must be
    installed, and the environment variable "OLD_Z3_SOLVER" must point to
    it.
    INCOMPATIBILITY.
  - The 'smt2' method has been renamed 'smt'.
    INCOMPATIBILITY.


Older news (also w.r.t. Isabelle2014):

* New (co)datatype package:
  - Renamed theorems:
      disc_corec ~> corec_disc
      disc_corec_iff ~> corec_disc_iff
      disc_exclude ~> distinct_disc
      disc_exhaust ~> exhaust_disc
      disc_map_iff ~> map_disc_iff
      sel_corec ~> corec_sel
      sel_exhaust ~> exhaust_sel
      sel_map ~> map_sel
      sel_set ~> set_sel
      sel_split ~> split_sel
      sel_split_asm ~> split_sel_asm
      strong_coinduct ~> coinduct_strong
      weak_case_cong ~> case_cong_weak
    INCOMPATIBILITY.
  - The rules "set_empty" have been removed. They are easy
    consequences of other set rules "by auto".
    INCOMPATIBILITY.
  - The rule "set_cases" is now registered with the "[cases set]"
    attribute. This can influence the behavior of the "cases" proof
    method when more than one case rule is applicable (e.g., an
    assumption is of the form "w : set ws" and the method "cases w"
    is invoked). The solution is to specify the case rule explicitly
    (e.g. "cases w rule: widget.exhaust").
    INCOMPATIBILITY.

* Old datatype package:
  - Renamed theorems:
      weak_case_cong ~> case_cong_weak
    INCOMPATIBILITY.

* Sledgehammer:
  - Minimization is now always enabled by default.
    Removed subcommand:
      min


Jasmin