Re: [isabelle] SMT.thy



Actually, I'm trying to use this import statement:

   imports Main "~~/src/HOL/SMT/SMT"

Thanks,
-john

On Feb 10, 2010, at 3:44 PM, John Matthews wrote:

Hello,

I'm trying to use the new "smt" proof method in Isabelle2009-1. Here's my theory header:

 theory test
 imports Main "~~/SMT/SMT"
 begin

However, Isabelle reports the following error when trying to load the SMT theory:

 *** Theory loader: failed to load "SMT" (unresolved "Z3", "SMT_Base")
 *** Theory loader: failed to load "Z3" (unresolved "SMT_Base")
 *** Undeclared class: "len"
*** At command "definition" (line 67 of "/Applications/Isabelle/ Isabelle/src/HOL/SMT/SMT_Base.thy").
 *** At command "theory".

Should I be loading SMT.thy some other way?

Thanks,
-john



Attachment: smime.p7s
Description: S/MIME cryptographic signature



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