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.




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