Re: [isabelle] Dependencies on constants



On 24/06/2010, at 7:05 AM, Jasmin Blanchette wrote:
> 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.

The difference may be because we're working on Isabelle 2009-1.

Cheers,
Gerwin




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