Re: [isabelle] Asking for Isabelle/Isar language specification



On Sun, 20 Feb 2011, anhlevn at cims.nyu.edu wrote:

I am Anh. In my current research, I parse and generate code in Isabelle/Isar. I really need the language specification, especially the syntax of Isabelle/Isar. In the current reference manual, the syntax of the language is not fully described and it's really hard to get it from separate parts of the manual. It would be really helpful if someone shows me some source to get that kind of information. Thank you very much

That's tricky, since Isabelle/Isar consists of pure semantics with some aspects modeled in concrete syntax (which can be extended in user space in compotationally complete ways). The isar-ref manual merely provides some reconstruction of syntactic forms that work in practice, but this cannot be complete by construction.

So the challange is to overcome the above requirement "I really need the language specification". What is your concrete application?


	Makarius





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