[isabelle] changing smt by automatic reasoning internal to Isabelle
Dear Isabelle users and experts,
In the rules for submissions to Archives of Formal Proofs, it is written
that "No use of the command smt_oracle". If I well understood, this means
that proofs cannot be done using either "apply smt" or "by smt" (please
correct me if I am wrong). This was also pointed out in Gerwin's Style
Guide (section: "Do not use smt in proofs you need to maintain over longer
(i) Is there an automatic way to change "smt" by some automatic reasoning
internal to Isabelle, e.g., metis, auto, simp?
(ii) In case of a negative answer for (i), which are the steps "by hand"
recommended for such a task?
José Manuel Rodríguez Caballero
arvutiteaduse instituut / Institute of Computer Science
Tartu Ülikool / University of Tartu
Personal Research Page: https://josephcmac.github.io/
This archive was generated by a fusion of
Pipermail (Mailman edition) and