Re: [isabelle] Dependencies on constants

Hi Rafal,

> What I want is some way of discovering (even really slowly) "this is the first occurrence of a given constant; before this theorem it did not exist before". In the case of "False" this would be HOL.False_def.

You might find the "Defs" table useful. E.g. try:

    ML {* Defs.all_specifications_of (Theory.defs_of @{theory}) *}

Most if not all constants get registered in this table when they are defined (or introduced with the "axiomatization" command).

A more recent and in many ways more powerful approach is to use

    ML {* Spec_Rules.get @{context} *}

The advantage of Spec_Rules is that it returns simplification rules for recursive functions rather than the raw definition, intro rules for (co)inductive predicates, etc.

I hope this helps.


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