equal
deleted
inserted
replaced
310 val name = "Provers/simpset"; |
310 val name = "Provers/simpset"; |
311 type T = simpset ref; |
311 type T = simpset ref; |
312 |
312 |
313 val empty = ref empty_ss; |
313 val empty = ref empty_ss; |
314 fun copy (ref ss) = (ref ss): T; (*create new reference!*) |
314 fun copy (ref ss) = (ref ss): T; (*create new reference!*) |
315 val finish = I; |
|
316 val prep_ext = copy; |
315 val prep_ext = copy; |
317 fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); |
316 fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); |
318 fun print _ (ref ss) = print_ss ss; |
317 fun print _ (ref ss) = print_ss ss; |
319 end; |
318 end; |
320 |
319 |