[isabelle-dev] Fwd: [isabelle] Exception in conv.ML

Stefan Berghofer berghofe at in.tum.de
Fri May 27 16:27:06 CEST 2011

Quoting Lawrence Paulson <lp15 at cam.ac.uk>:
> But I could be wrong, as such checks may be done elsewhere. Does  
> anybody else have a suggestion?

Hi Larry and Andreas,

there is another occurrence of gconv_rule in Provers/blast.ML
(in function timing_depth_tac). Since the exception is thrown
when invoking blast, this occurrence of gconv_rule may be the


More information about the isabelle-dev mailing list