equal
deleted
inserted
replaced
172 struct |
172 struct |
173 val name = "Sequents/prover"; |
173 val name = "Sequents/prover"; |
174 type T = pack ref; |
174 type T = pack ref; |
175 val empty = ref empty_pack |
175 val empty = ref empty_pack |
176 fun copy (ref pack) = ref pack; |
176 fun copy (ref pack) = ref pack; |
|
177 val finish = I; |
177 val prep_ext = copy; |
178 val prep_ext = copy; |
178 fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2)); |
179 fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2)); |
179 fun print _ (ref pack) = print_pack pack; |
180 fun print _ (ref pack) = print_pack pack; |
180 end; |
181 end; |
181 |
182 |