equal
deleted
inserted
replaced
16 |
16 |
17 |
17 |
18 *** HOL *** |
18 *** HOL *** |
19 |
19 |
20 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
20 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
21 respectively. INCOMPATBILITY. |
21 respectively. INCOMPATIBILITY. |
22 |
22 |
23 * Constant "split" has been merged with constant "prod_case"; names |
23 * Constant "split" has been merged with constant "prod_case"; names |
24 of ML functions, facts etc. involving split have been retained so far, |
24 of ML functions, facts etc. involving split have been retained so far, |
25 though. INCOMPATIBILITY. |
25 though. INCOMPATIBILITY. |
26 |
26 |