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



On 08/05/2011 12:13 AM, Alfio Martini wrote:
Great!! Thanks for the quick reply!

f.simps(2)

You can also name the rules at definition time:

fun/primrec f :: "..."
where
  name1: "..."
| name2: "..."


Alex





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