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



Great!! Thanks for the quick reply!

On Thu, Aug 4, 2011 at 7:01 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote:

> f.simps(2)
>
> On Thu, Aug 4, 2011 at 5:39 PM, Alfio Martini <alfio.martini at acm.org>
> 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
> >
> >
>



-- 
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.