equal
deleted
inserted
replaced
30 sel_set ~> set_sel |
30 sel_set ~> set_sel |
31 sel_split ~> split_sel |
31 sel_split ~> split_sel |
32 sel_split_asm ~> split_sel_asm |
32 sel_split_asm ~> split_sel_asm |
33 strong_coinduct ~> coinduct_strong |
33 strong_coinduct ~> coinduct_strong |
34 weak_case_cong ~> case_cong_weak |
34 weak_case_cong ~> case_cong_weak |
|
35 INCOMPATIBILITY. |
|
36 - The rule "set_cases" is registered with the "[cases set]" |
|
37 attribute. This can influence the behavior of the "cases" proof |
|
38 method when more than one case rule is applicable (e.g., an |
|
39 assumption is of the form "w : set ws" and the method "cases w" |
|
40 is invoked). The solution is to specify the case rule explicitly |
|
41 (e.g. "cases w rule: widget.exhaust"). |
35 INCOMPATIBILITY. |
42 INCOMPATIBILITY. |
36 |
43 |
37 * Old datatype package: |
44 * Old datatype package: |
38 - Renamed theorems: |
45 - Renamed theorems: |
39 weak_case_cong ~> case_cong_weak |
46 weak_case_cong ~> case_cong_weak |