Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem sledgehammer/presburger

Email Gateway (Aug 22 2022 at 18:24):

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: Apr 25 2024 at 12:23 UTC