Re: [isabelle] Parser in ML
The answer is yes.
I believe there all the information that you need can be found on this page:
It is not entirely trivial to set up.
On 12 Dec 2013, at 14:56, li yongjian <lyj238 at gmail.com> wrote:
> 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