Re: [isabelle] Dependencies on constants

On 24/06/10 07:05, Jasmin Blanchette wrote:
Am 23.06.2010 um 18:44 schrieb Rafal Kolanski:

I've investigated Spec_Rules. It works as advertised for "definition" and "constdefs", however the primrec/recdef/function/fun sadly do not register their constants in this manner.


     $ grep -l Spec_Rules ~/isabelle/src/HOL/Tools/*{,/*}

I see primrec, recdef, and function/fun in there. Lukas's predicate compiler uses "Spec_Rules" to find equational specifications, so it must be working. Nitpick uses it already for the "(co)inductive" package and it's definitely working.

I apologise, I failed to mention I'm on Isabelle 2009-1, working with on the L4.verified repository. To me it looked like this:

[~/repos/l4.verified/isabelle]# rgrep -l Spec_Rules *

Sorry. I'm glad Isabelle is, as usual, headed in the right direction. Although as usual I'm a few steps behind.

I've finally hacked my way through the Defs interface. It was cryptic, but consistent. Thank you for your help!


Rafal Kolanski.

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