Jørgen Villadsen
2018-09-01 12:46:37 UTC
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... :-)
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... :-)