Re: [isabelle] novice problem about loading theory file



Dear all,

 

Thanks for your help.

 

I first tried the use the "logic image HOL-Complex rather than HOL" by starting Isabelle with the command"

Isabelle -l HOL-Complex

 

And it reports "unkonwn logic "HOL-Complex";

 

So I follow the other way, i.e., by import the real.thy explicitly by entering command

imports "~~/src/HOL/Real/Real"

 

It seems OK with the following message given:

theory FirstTry = {Main, Lubs, Quotient, Rational, PReal, RealDef, RComplete, RealPow, Real, #}

 

Hence I suppose that is the right way for me to use real number in Isabelle, though currently I have not started the proof.

 

I guess that the reason that the first way fails is that I am using Isabelle2005 which may have different name for real theory.

 

Regards

Chunqing



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