Re: [isabelle] isar-keywords



On Tue, 30 Mar 2010, Omar Montano Rivas wrote:

*** Stopper may not occur in input of finite scan!
*** At command "<malformed>" (line 29 of "...").

Is it possible to build B from the command line using "isabelle make" to get all the benefits of document preparation (latex, html, etc...)? Is the problem related with the isar-keyword file or it is something else?

To me this looks more like a problem in the outer syntax parser for your newly defined command. Can I see your ML definition for the syntax?


	Makarius






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