Quoting Lawrence Paulson <[email protected]>:
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 culprit. Greetings, Stefan _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
