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