Re: [isabelle] SMT.thy
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"
Note that in any case "Main" does not need to be imported, because it
is already contained in SMT.
John Matthews wrote:
> Actually, I'm trying to use this import statement:
> imports Main "~~/src/HOL/SMT/SMT"
> On Feb 10, 2010, at 3:44 PM, John Matthews wrote:
> >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/
> > *** At command "theory".
> >Should I be loading SMT.thy some other way?
This archive was generated by a fusion of
Pipermail (Mailman edition) and