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