equal
deleted
inserted
replaced
73 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
73 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
74 token category instead. |
74 token category instead. |
75 |
75 |
76 |
76 |
77 *** HOL *** |
77 *** HOL *** |
|
78 |
|
79 * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for |
|
80 single-step rewriting with subterm selection based on patterns. |
78 |
81 |
79 * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
82 * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
80 type, so in particular on "real" and "complex" uniformly. |
83 type, so in particular on "real" and "complex" uniformly. |
81 Minor INCOMPATIBILITY: type constraints may be needed. |
84 Minor INCOMPATIBILITY: type constraints may be needed. |
82 |
85 |