Hi list,

There are well-known implementation techniques for depth-first theorem
proving, using continuation-passing style (success/failure
continuations). But these techniques do not easily allow the building
of a proof witness. This is nice when you have a working proof-search
procedure but not when you're still playing with a logic, trying to
find the right procedure or more generally when you just want an
interactive prover.

I've started to look for a way to define rules as tactics in such a
way that these core functions can be used with or without a proof
witness construction procedure. I've had enough for today and I wanted
to know if anyone done that or knows a link to anything like that.

Any idea?
-- 
David