Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem sledgehammer/presburger


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC