equal
deleted
inserted
replaced
169 attribute. This can influence the behavior of the "cases" proof |
169 attribute. This can influence the behavior of the "cases" proof |
170 method when more than one case rule is applicable (e.g., an |
170 method when more than one case rule is applicable (e.g., an |
171 assumption is of the form "w : set ws" and the method "cases w" |
171 assumption is of the form "w : set ws" and the method "cases w" |
172 is invoked). The solution is to specify the case rule explicitly |
172 is invoked). The solution is to specify the case rule explicitly |
173 (e.g. "cases w rule: widget.exhaust"). |
173 (e.g. "cases w rule: widget.exhaust"). |
|
174 INCOMPATIBILITY. |
|
175 - Renamed theories: |
|
176 BNF_Comp ~> BNF_Composition |
|
177 BNF_FP_Base ~> BNF_Fixpoint_Base |
|
178 BNF_GFP ~> BNF_Greatest_Fixpoint |
|
179 BNF_LFP ~> BNF_Least_Fixpoint |
|
180 BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions |
|
181 Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions |
174 INCOMPATIBILITY. |
182 INCOMPATIBILITY. |
175 |
183 |
176 * Old datatype package: |
184 * Old datatype package: |
177 - The old 'datatype' command has been renamed 'old_datatype', and |
185 - The old 'datatype' command has been renamed 'old_datatype', and |
178 'rep_datatype' has been renamed 'old_rep_datatype'. They are |
186 'rep_datatype' has been renamed 'old_rep_datatype'. They are |