equal
deleted
inserted
replaced
50 lemma "P (x::'a)" and "Q (y::'a::bar)" |
50 lemma "P (x::'a)" and "Q (y::'a::bar)" |
51 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
51 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
52 |
52 |
53 |
53 |
54 *** HOL *** |
54 *** HOL *** |
|
55 |
|
56 * Renamed some facts on canonical fold on lists, in order to avoid problems |
|
57 with interpretation involving corresponding facts on foldl with the same base names: |
|
58 |
|
59 fold_set_remdups ~> fold_set_fold_remdups |
|
60 fold_set ~> fold_set_fold |
|
61 fold1_set ~> fold1_set_fold |
|
62 |
|
63 INCOMPATIBILITY. |
55 |
64 |
56 * 'set' is now a proper type constructor. Definitions mem_def and Collect_def |
65 * 'set' is now a proper type constructor. Definitions mem_def and Collect_def |
57 have disappeared. INCOMPATIBILITY, rephrase sets S used as predicates by |
66 have disappeared. INCOMPATIBILITY, rephrase sets S used as predicates by |
58 `%x. x : S` and predicates P used as sets by `{x. P x}`. For typical proofs, |
67 `%x. x : S` and predicates P used as sets by `{x. P x}`. For typical proofs, |
59 it is often sufficent to prune any tinkering with former theorems mem_def |
68 it is often sufficent to prune any tinkering with former theorems mem_def |