[isabelle] Still no smt commands allowed in AFP submissions?



Dear Isabelle experts,

When I am checking the AFP submission guidelines, it requires no smt command in proofs. I thought proof reconstructions for smt solvers should be quite mature now. Shall I still need to eliminate all smt commands from my proofs before submission to AFP?

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.