equal
deleted
inserted
replaced
920 val name = "Provers/claset"; |
920 val name = "Provers/claset"; |
921 type T = claset ref; |
921 type T = claset ref; |
922 |
922 |
923 val empty = ref empty_cs; |
923 val empty = ref empty_cs; |
924 fun copy (ref cs) = (ref cs): T; (*create new reference!*) |
924 fun copy (ref cs) = (ref cs): T; (*create new reference!*) |
|
925 val finish = I; |
925 val prep_ext = copy; |
926 val prep_ext = copy; |
926 fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); |
927 fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); |
927 fun print _ (ref cs) = print_cs cs; |
928 fun print _ (ref cs) = print_cs cs; |
928 end; |
929 end; |
929 |
930 |