Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer and HOL-Complex

view this post on Zulip Email Gateway (Aug 18 2022 at 12:17):

From: Matthias Berg <berg@cs.uni-sb.de>
Hi,

I have a problem to invoke sledgehammer in HOL-Complex with Isabelle2008:

theory test imports Complex_Main begin
lemma "(1::nat)+1 = 2"
sledgehammer;

gives the Error:

*** Attempt to perform non-trivial merge of theories:
*** {..., Extraction, Relation_Power, Refute, SAT, ATP_Linkup}
*** {..., IntDiv, NatBin, Groebner_Basis, Arith_Tools, Dense_Linear_Order}
*** At command "sledgehammer".

The following works, where I import just Main:

theory test imports Main begin
lemma "(1::nat)+1 = 2"
sledgehammer;

Thanks,
Matthias

view this post on Zulip Email Gateway (Aug 18 2022 at 12:18):

From: Tobias Nipkow <nipkow@in.tum.de>
I have not seen a reply to your email and I am not familiar enough with
the s/h implementation to answer it, but I can at least tell you that
with the current development version it works.

Tobias

Matthias Berg schrieb:

Last updated: May 03 2024 at 08:18 UTC