Re: [isabelle] thm dependencies



On Tue, 25 Oct 2005, John Matthews wrote:

> Here is the SML code I wrote to extract the list of external oracle tags
> used in the proof of a theorem. Am I using any deprecated functions?

This looks fine.


> text {* This will let us view the tagged oracles using surface syntax. 
> *}
>    in map (fn (oracle,formula) => (oracle, Sign.string_of_term thy 

Just a minor point concerning ``surface syntax'': using the theory context
of a theorem is a fair approximation if this is just for diagnostics.  
For realistic output of formal entities one should usually use the static
proof context of the invoking command, with ProofContext.string_of_term
etc.  There is also an abstract Pretty.pp concept for passing aroung
syntactic context for pretty printing output.


	Makarius





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