Re: [isabelle] File.use function

On Mon, 1 May 2006, Clément Hurlin wrote:

> When executing, it now says that 'proof_inst' and 'proof_congr' are not 
> declared. I guess that when calling use, the context of the call isn't 
> inherited. But this is bizarre since it works inside an interactive 
> session...

Note that 'use' is a descendent of the venerable 'eval' of LISP, which 
always operates on the toplevel environment.  In fact use/eval is some 
kind of magic that should not be invoked only in very special situations.

Better stay with ordinary value oriented functions ... -> theory -> theory 
of Proof.context -> Proof.context (or mutable references as a last 


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