equal
deleted
inserted
replaced
12 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list |
12 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list |
13 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory |
13 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory |
14 (*etc*) |
14 (*etc*) |
15 end; |
15 end; |
16 |
16 |
17 structure KEStore_Elems: KESTORE_ELEMS = |
17 structure Test_KEStore_Elems: KESTORE_ELEMS = |
18 struct |
18 struct |
19 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
19 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
20 |
20 |
21 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*) |
21 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*) |
22 structure Data = Theory_Data ( |
22 structure Data = Theory_Data ( |