equal
deleted
inserted
replaced
355 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
355 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
356 one_case. |
356 one_case. |
357 |
357 |
358 * Discontinued configuration option "syntax_positions": atomic terms |
358 * Discontinued configuration option "syntax_positions": atomic terms |
359 in parse trees are always annotated by position constraints. |
359 in parse trees are always annotated by position constraints. |
|
360 |
|
361 * HOL/Library/Set_Algebras.thy: Addition and multiplication on sets |
|
362 are expressed via type classes again. The special syntax |
|
363 \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant |
|
364 setsum_set, which is now subsumed by Big_Operators.setsum. |
|
365 INCOMPATIBILITY. |
360 |
366 |
361 * New theory HOL/Library/DAList provides an abstract type for |
367 * New theory HOL/Library/DAList provides an abstract type for |
362 association lists with distinct keys. |
368 association lists with distinct keys. |
363 |
369 |
364 * 'datatype' specifications allow explicit sort constraints. |
370 * 'datatype' specifications allow explicit sort constraints. |