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 * Consolidated various theorem names relating to Finite_Set.fold combinator: |
|
64 inf_INFI_fold_inf ~> inf_INF_fold_inf |
|
65 sup_SUPR_fold_sup ~> sup_SUP_fold_sup |
|
66 INFI_fold_inf ~> INF_fold_inf |
|
67 SUPR_fold_sup ~> SUP_fold_sup |
|
68 union_set ~> union_set_fold |
|
69 minus_set ~> minus_set_fold |
|
70 |
|
71 INCOMPATIBILITY. |
62 |
72 |
63 * Consolidated theorem names concerning fold combinators: |
73 * Consolidated theorem names concerning fold combinators: |
64 INFI_set_fold ~> INF_set_fold |
74 INFI_set_fold ~> INF_set_fold |
65 SUPR_set_fold ~> SUP_set_fold |
75 SUPR_set_fold ~> SUP_set_fold |
66 INF_code ~> INF_set_foldr |
76 INF_code ~> INF_set_foldr |