Re: [isabelle] SMT.thy



Hello John,

Thanks for reporting this bug; it will be fixed in newer versions of
Isabelle. As for Isabelle2009-1, there are two possible workarounds
(the first one is the recommended way):

1) Build the HOL-SMT image by (at the Isabelle2009-1 directory):

      ./build -m HOL-SMT HOL

   and load this when using SMT instead of the default HOL image.
   With this method, you may drop the path to the SMT theory; the
   import line may thus read "imports SMT".

2) Manually modify the file "~~/src/HOL/SMT/SMT_Base.thy", i.e.,
   change the line starting with "imports" into

     imports Real "~~/src/HOL/Word/Word"
       "~~/src/HOL/Decision_Procs/Dense_Linear_Order"

Note that in any case "Main" does not need to be imported, because it
is already contained in SMT.

Regards,
Sascha


John Matthews wrote:
> 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
> >
> >
> 







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