* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
