Re: [isabelle] Sledgehammer and HOL-Complex



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:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.