[isabelle] Parser in ML

Dear  Isabelle experts:
  Recently I meet a case study where I need:
  a parser that accepts a foreign text file and transforms it into a thy
file and
  automatically generate some proofs.

   I want to know whether poly-ML system that writes Isabelle have some
support for writing a parser.
   I have read Larry's ML-book, and after reading the last two chapters,  I
think that I can create a parser using suppot from Isabelle system.

  I know that Objcaml has a support for YACC to generate a parse, and I
prefer this Yacc approach. I want to know whther Poly ML supports YACC to
create a parser?

yongjian Li

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.