equal
deleted
inserted
replaced
65 * Discontinued empty name bindings in 'axiomatization'. |
65 * Discontinued empty name bindings in 'axiomatization'. |
66 INCOMPATIBILITY. |
66 INCOMPATIBILITY. |
67 |
67 |
68 |
68 |
69 *** HOL *** |
69 *** HOL *** |
|
70 |
|
71 * Code generator: |
|
72 * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'. |
|
73 * 'code_identifier' declares name hints for arbitrary identifiers in generated code, |
|
74 subsuming 'code_modulename'. |
|
75 See the Isar reference manual for syntax diagrams, and the HOL theories for examples. |
70 |
76 |
71 * Library/Polynomial.thy: |
77 * Library/Polynomial.thy: |
72 * Use lifting for primitive definitions. |
78 * Use lifting for primitive definitions. |
73 * Explicit conversions from and to lists of coefficients, used for generated code. |
79 * Explicit conversions from and to lists of coefficients, used for generated code. |
74 * Replaced recursion operator poly_rec by fold_coeffs. |
80 * Replaced recursion operator poly_rec by fold_coeffs. |