| changeset 74561 | 8e6c973003c8 |
| parent 74287 | f79dfc7656ae |
| child 78049 | d7395ef81292 |
| 74560:5c8177fd1295 | 74561:8e6c973003c8 |
|---|---|
34 |
34 |
35 structure Data = Generic_Data |
35 structure Data = Generic_Data |
36 ( |
36 ( |
37 type T = def Item_Net.T; |
37 type T = def Item_Net.T; |
38 val empty : T = Item_Net.init eq_def (single o #lhs); |
38 val empty : T = Item_Net.init eq_def (single o #lhs); |
39 val extend = I; |
|
40 val merge = Item_Net.merge; |
39 val merge = Item_Net.merge; |
41 ); |
40 ); |
42 |
41 |
43 fun declare_def lhs eq lthy = |
42 fun declare_def lhs eq lthy = |
44 let |
43 let |