From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
In the attached theory "sledgehammer" suggests "by presburger" with specific milliseconds reported - but it does not work - any ideas?
Sometimes "by meson" is suggested and it works.
Regards,
Jørgen
PS - Same result in Isabelle2017... :-)
Problem.thy
Last updated: Nov 21 2024 at 12:39 UTC