<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<div><div>I'm sorry I sent the last message truncated. Here is the rest of the message:<br></div><div dir="auto"><br></div><div dir="auto">fun ring_tac add_ths del_ths ctxt =<br> Object_Logic.full_atomize_tac ctxt<br> THEN' presimplify ctxt add_ths del_ths<br> THEN' CSUBGOAL (fn (p, i) =><br> resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p<br> in case get_ring_ideal_convs ctxt form of<br> NONE => Thm.reflexive form<br> | SOME thy => #ring_conv thy ctxt form<br> end] i<br> handle TERM _ => no_tac<br> | CTERM _ => no_tac<br> | THM _ => no_tac);</div><div dir="auto"><br></div><div dir="auto">I do not see how debug this system like I could with printing state in imperative languages, so I'm lost at this point.<br></div><div dir="auto"><br></div><div dir="auto">Best,<br></div><div>Christian Weinz<br></div></div> </body>
</html>