Re: [isabelle] Accessing (individual) simplification rules of function definitions


On Thu, Aug 4, 2011 at 5:39 PM, Alfio Martini <alfio.martini at> wrote:
> Dear Isabelle Users,
> Usually, after a function f has been defined via fun or primrec, its
> defining equations are available under the name
> f.simps as theorems, e.g., thm "f.simps".
> However, how could I access specifically each one of these equations
> (simplification rules)?
> I tried something as f.simps_1 (after seeing the trace example in the
> tutorial), f.simps_2,  etc., but
> it did not work.
> Thanks!
> --
> Alfio Ricardo Martini
> PhD in Computer Science (TU Berlin)
> Associate Professor at Faculty of Informatics (PUCRS)
> Porto Alegre - RS - Brasil

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