equal
deleted
inserted
replaced
61 wmsI2'' : thm, |
61 wmsI2'' : thm, |
62 wmsI1 : thm, |
62 wmsI1 : thm, |
63 reduction_pair : thm |
63 reduction_pair : thm |
64 } |
64 } |
65 |
65 |
66 structure Multiset_Setup = TheoryDataFun |
66 structure Multiset_Setup = Theory_Data |
67 ( |
67 ( |
68 type T = multiset_setup option |
68 type T = multiset_setup option |
69 val empty = NONE |
69 val empty = NONE |
70 val copy = I; |
|
71 val extend = I; |
70 val extend = I; |
72 fun merge _ (v1, v2) = if is_some v2 then v2 else v1 |
71 fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *) |
73 ) |
72 ) |
74 |
73 |
75 val multiset_setup = Multiset_Setup.put o SOME |
74 val multiset_setup = Multiset_Setup.put o SOME |
76 |
75 |
77 fun undef x = error "undef" |
76 fun undef x = error "undef" |