src/Sequents/prover.ML
changeset 12311 ce5f9e61c037
parent 12123 739eba13e2cd
child 13105 3d1e7a199bdc
equal deleted inserted replaced
12310:26407b087c8e 12311:ce5f9e61c037
   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;
       
   178   val prep_ext = copy;
   177   val prep_ext = copy;
   179   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   178   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   180   fun print _ (ref pack) = print_pack pack;
   179   fun print _ (ref pack) = print_pack pack;
   181   end;
   180   end;
   182 
   181