Re: [isabelle] Isabelle Point Releases?



On Fri, 27 Apr 2007, Thomas Bleher wrote:

> A small irregularity I just encountered: 'use_thy "SomeTheory"' only 
> works in interactive mode, not when creating PDFs. For these, I have to 
> wrap the command in 'ML {* *}'. Would be nice to make this consistent.

I don't understand what you are trying to do here.  Importing theories 
into the current theory works via the "imports" header specification.  
The use_thy ML function should only occur in ROOT.ML to tell the system 
where to start processing theories (it also allows to adjust some external 
flags, such as no_document).


	Makarius





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