Tobias
On 26/05/2020 17:12, Manuel Eberl wrote:
If I recall correctly, Z3 is open source and bundled with Isabelle, so there is no problem in that regard. The only problem I can think of is that these proofs are unreadable and tend to break frequently. But the same is true for "metis" proofs. I avoid both of them wherever I can for that reason, but it would be unrealistic to set this as a general policy. So unless there is some problem with it that I am unaware of, I think our policy should be "accepted, but perhaps frowned upon just a little bit by some people". :) Manuel On 26/05/2020 17:09, Lawrence Paulson wrote:What is our policy on use of the smt method at the moment? Prohibited, frowned upon, okay? Getting rid of it can take a lot of work. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
