equal
deleted
inserted
replaced
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. |
35 INCOMPATIBILITY. |
36 - The rule "set_cases" is registered with the "[cases set]" |
36 - The rules "set_empty" have been removed. They are easy |
|
37 consequences of other set rules "by auto". |
|
38 INCOMPATIBILITY. |
|
39 - The rule "set_cases" is now registered with the "[cases set]" |
37 attribute. This can influence the behavior of the "cases" proof |
40 attribute. This can influence the behavior of the "cases" proof |
38 method when more than one case rule is applicable (e.g., an |
41 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" |
42 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 |
43 is invoked). The solution is to specify the case rule explicitly |
41 (e.g. "cases w rule: widget.exhaust"). |
44 (e.g. "cases w rule: widget.exhaust"). |