I have a question regarding the use of keyword files in
Isabelle2009-1. I have developed a theory A and obtained a keyword
file ("isar-keyword-C.el") for my new command C using the method
described in the isabelle's ML programming tutorial (http://isabelle.in.tum.de/nominal/activities/idp/
). Now I want to build a new theory B on top of A using the command C.
I have placed the file "isar-keyword-C.el" in "~/.isabelle/etc" and
the command "isabelle emacs -k C" starts a new proof general session
where the command C is being perfectly recognized. But when I try to
build the theory B from the command line with "isabelle make" I get an
error at the point where the new command C is used.
*** 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
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and