Re: [isabelle] Complex_Main



On Fri, 27 Mar 2009, Jens Doll wrote:

I am having a problem with the installation instructions. I downloaded the
cygwin Complex_Main and save it to the /usr/local. Then it was tarred with
tar -xzf HOL-*gz. Now Isabelle still says:

*** Could not find theory file "Complex_Main.thy" in ".", "/home/Jens",
"$ISABELLE_HOME/src/HOL/Library"
*** Theory loader: the error(s) above occurred while examining theory
"Complex_Main"
*** At command "theory".

What could be wrong?

By "Isabelle" you probably mean your Proof General session. Here you need to say that you want to use the "HOL-Complex" logic instead of the default one "HOL".


	Makarius






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