equal
deleted
inserted
replaced
72 |
72 |
73 list.exhaust [case_product nat.exhaust] |
73 list.exhaust [case_product nat.exhaust] |
74 |
74 |
75 produces a rule which can be used to perform case distinction on both |
75 produces a rule which can be used to perform case distinction on both |
76 a list and a nat. |
76 a list and a nat. |
|
77 |
|
78 |
|
79 * Nitpick: |
|
80 - Fixed infinite loop caused by the 'peephole_optim' option and affecting |
|
81 'rat' and 'real'. |
77 |
82 |
78 |
83 |
79 *** FOL *** |
84 *** FOL *** |
80 |
85 |
81 * New "case_product" attribute (see HOL). |
86 * New "case_product" attribute (see HOL). |