[isabelle] SMT.thy



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.