equal
deleted
inserted
replaced
63 * Concrete syntax for case expressions includes constraints for source |
63 * Concrete syntax for case expressions includes constraints for source |
64 positions, and thus produces Prover IDE markup for its bindings. |
64 positions, and thus produces Prover IDE markup for its bindings. |
65 INCOMPATIBILITY for old-style syntax translations that augment the |
65 INCOMPATIBILITY for old-style syntax translations that augment the |
66 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
66 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
67 one_case. |
67 one_case. |
|
68 |
|
69 * Discontinued configuration option "syntax_positions": atomic terms |
|
70 in parse trees are always annotated by position constraints. |
68 |
71 |
69 * Finite_Set.fold now qualified. INCOMPATIBILITY. |
72 * Finite_Set.fold now qualified. INCOMPATIBILITY. |
70 |
73 |
71 * Renamed some facts on canonical fold on lists, in order to avoid problems |
74 * Renamed some facts on canonical fold on lists, in order to avoid problems |
72 with interpretation involving corresponding facts on foldl with the same base names: |
75 with interpretation involving corresponding facts on foldl with the same base names: |