[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
I tried something as f.simps_1 (after seeing the trace example in the
tutorial), f.simps_2, etc., but
it did not work.
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