Re: [isabelle] simp matching depends on lexicographic variable naming



Am 13/02/2013 08:36, schrieb Gottfried Barrow:
> When I do a command "apply simp", is there a command to tell me what rules it
> applied for that command? All I know about is "print_simpset". A great debugger
> tool would be able to single step through the simp rules for an "apply simp".

Such a tool is in the making. For the time being you can prefix your "apply
simp" by "using [[simp_trace]]". This gives you a very detailed trace, probably
much more than what you want.

Tobias





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