Hi, I'm wondering whether anyone has a tool to generate output from a Larch interface specification that can be read by the Larch Prover. I'm working on proving relationships between two Larch/ML specifications, and so far have been generating the LP input by hand. I'm now working on automating it, and would like to hear about any other work in this direction. Thanks! Amy Moormann Zaremski amy+@cs.cmu.edu