[isabelle] debugging Isar

I have a long and complex tactic (long and complex meaning I started work on it over a year ago, and I don't yet know whether it works on more than one example).

But it does work on one example, in ML
(as in
Goal "..." ; byall ...tacs ; )

When I package it up as an Isar method, it doesn't work.
If it didn't work in ML I would do

val state = topthm()

and then go through the code step-by-step, to see where it fails.

Trying this in Isar, with the obligatory ML {* ... *} around each step,

ML {* val state = topthm () *}
val state =
  "PROP No_goal_has_been_supplied ==> PROP No_goal_has_been_supplied"

which obviously won't help.

How do I debug such a thing in Isar?


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