equal
deleted
inserted
replaced
26 * Command and antiquotation "value" provide different evaluation slots (again), |
26 * Command and antiquotation "value" provide different evaluation slots (again), |
27 where the previous strategy (nbe after ML) serves as default. |
27 where the previous strategy (nbe after ML) serves as default. |
28 Minor INCOMPATIBILITY. |
28 Minor INCOMPATIBILITY. |
29 |
29 |
30 * New (co)datatype package: |
30 * New (co)datatype package: |
|
31 - The 'datatype_new' command has been renamed 'datatype'. The old command of |
|
32 that name is now called 'old_datatype'. See 'isabelle doc datatypes' for |
|
33 information on porting. |
31 - Renamed theorems: |
34 - Renamed theorems: |
32 disc_corec ~> corec_disc |
35 disc_corec ~> corec_disc |
33 disc_corec_iff ~> corec_disc_iff |
36 disc_corec_iff ~> corec_disc_iff |
34 disc_exclude ~> distinct_disc |
37 disc_exclude ~> distinct_disc |
35 disc_exhaust ~> exhaust_disc |
38 disc_exhaust ~> exhaust_disc |
56 is invoked). The solution is to specify the case rule explicitly |
59 is invoked). The solution is to specify the case rule explicitly |
57 (e.g. "cases w rule: widget.exhaust"). |
60 (e.g. "cases w rule: widget.exhaust"). |
58 INCOMPATIBILITY. |
61 INCOMPATIBILITY. |
59 |
62 |
60 * Old datatype package: |
63 * Old datatype package: |
|
64 - The old 'datatype' command has been renamed 'old_datatype', and |
|
65 'rep_datatype' has been renamed 'old_rep_datatype'. See |
|
66 'isabelle doc datatypes' for information on porting. |
61 - Renamed theorems: |
67 - Renamed theorems: |
62 weak_case_cong ~> case_cong_weak |
68 weak_case_cong ~> case_cong_weak |
63 INCOMPATIBILITY. |
69 INCOMPATIBILITY. |
64 |
70 |
65 * Sledgehammer: |
71 * Sledgehammer: |