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



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.