equal
deleted
inserted
replaced
57 lemma "P (x::'a)" and "Q (y::'a::bar)" |
57 lemma "P (x::'a)" and "Q (y::'a::bar)" |
58 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
58 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
59 |
59 |
60 |
60 |
61 *** HOL *** |
61 *** HOL *** |
|
62 |
|
63 * Concrete syntax for case expressions includes constraints for source |
|
64 positions, and thus produces Prover IDE markup for its bindings. |
|
65 INCOMPATIBILITY for old-style syntax translations that augment the |
|
66 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
|
67 one_case. |
62 |
68 |
63 * Finite_Set.fold now qualified. INCOMPATIBILITY. |
69 * Finite_Set.fold now qualified. INCOMPATIBILITY. |
64 |
70 |
65 * Renamed some facts on canonical fold on lists, in order to avoid problems |
71 * Renamed some facts on canonical fold on lists, in order to avoid problems |
66 with interpretation involving corresponding facts on foldl with the same base names: |
72 with interpretation involving corresponding facts on foldl with the same base names: |