+++++++++++++++++++++++++++++++++++++++++++++++++++++

We thank the referees for the detailed comments.

We have taken almost everything into account so here we just list the
things that we did *not* do.

The referee suggested that we replace "x IN S" with "S x" uniformly to
make the connections between set membership and predicates clearer. We
have not done this as the two are not equivalent in HOL4, although
they are provably equivalent in the sense that one holds iff the
second holds.

One referee also suggested replacing "Meta-theory" in the title but we
are confident that "Meta-theory of dual tableaux" is specific enough.

We also ignored the comment beginning "- p.22, -4, Definition 27. The
term 'idt_R-successor' is not fortunate" because we could not
understand what the reviewer was trying to say. We would be happy to
fix it if he or she could clarify the objeciton.

Finally, please can you ensure that Mel cites our work properly. He
mentions ``proof theory'' in his citation on page 3 line 5, but this
is not really accurate as our contribution mimics his in using the
semantics. His citation should also say ``Dawson and Gor\'e'' not just
``Gor\'e''.

raj and jeremy

+++++++++++++++++++++++++++++++++++++++++++++++++++++