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.


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