equal
deleted
inserted
replaced
32 * Diagnostic command 'print_interps' prints interpretations in proofs |
32 * Diagnostic command 'print_interps' prints interpretations in proofs |
33 in addition to interpretations in theories. |
33 in addition to interpretations in theories. |
34 |
34 |
35 |
35 |
36 *** HOL *** |
36 *** HOL *** |
|
37 |
|
38 * Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax |
|
39 in Library/State_Monad has been changed to avoid ambiguities. |
|
40 INCOMPATIBILITY. |
37 |
41 |
38 * code generator: export_code without explicit file declaration prints |
42 * code generator: export_code without explicit file declaration prints |
39 to standard output. INCOMPATIBILITY. |
43 to standard output. INCOMPATIBILITY. |
40 |
44 |
41 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
45 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |