[isabelle-dev] Application of method algebra fails

[christian at madez.de]

I'm sorry I sent the last message truncated. Here is the rest of the message:

fun ring_tac add_ths del_ths ctxt =
  Object_Logic.full_atomize_tac ctxt
  THEN' presimplify ctxt add_ths del_ths
  THEN' CSUBGOAL (fn (p, i) =>
    resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p
          in case get_ring_ideal_convs ctxt form of
           NONE => Thm.reflexive form
          | SOME thy => #ring_conv thy ctxt form
          end] i
      handle TERM _ => no_tac
        | CTERM _ => no_tac
        | THM _ => no_tac);
I do not see how debug this system like I could with printing state in imperative languages, so I'm lost at this point.

Best,
Christian Weinz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230322/27e00690/attachment.htm>