Re: [isabelle] thm dependencies

I am also interested in this question. Similarly, how to I extract the list of external oracles used in the proof of a tagged theorem, when theorem dependencies are turned off?


On Oct 24, 2005, at 5:52 PM, Sean McLaughlin wrote:


  I'd like a way to extract the theorem dependencies of a theorem.
I know Isabelle has a great facility for plotting these deps with
"thm_deps", but is there a way to just extract a tree of dependencies
(that could be topologically sorted, say).

Same question for entire theories: there is the command
ML {* print_theory (theory "Set") *}
which prints the theorems in alphabetical order.  Is there a way
to print them, say, in the order of definition?
I looked in theory.ML, but the type theory doesn't have
any reference to type term.thm.

Thanks, for this an my previous questions!


On Oct 24, 2005, at 8:11 AM, Makarius wrote:

On Sun, 23 Oct 2005, Sean McLaughlin wrote:

However, when I construct a term myself, it doesn't

ML {* term_tvars (read "INTER") *}
val it = [] : (Term.indexname * Term.sort) list

Just note that the read function belongs to the legacy goal package, it may refer to an unexpected context. Use Sign.read_term (the_context ())
instead -- in production code the theory is even to be passed as an
explicit value.

Unlike Larry, I do recommend ML experiments within ProofGeneral/isar.


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