equal
deleted
inserted
replaced
14 consistent view on symbols, while raw explode (or String.explode) |
14 consistent view on symbols, while raw explode (or String.explode) |
15 merely give a byte-oriented representation. |
15 merely give a byte-oriented representation. |
16 |
16 |
17 |
17 |
18 *** HOL *** |
18 *** HOL *** |
|
19 |
|
20 * code generator: export_code without explicit file declaration prints |
|
21 to standard output. INCOMPATIBILITY. |
19 |
22 |
20 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
23 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
21 respectively. INCOMPATIBILITY. |
24 respectively. INCOMPATIBILITY. |
22 |
25 |
23 * Constant "split" has been merged with constant "prod_case"; names |
26 * Constant "split" has been merged with constant "prod_case"; names |