[isabelle] Sledgehammer and HOL-Complex



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.