[isabelle] novice problem about loading theorey file



Dear all,

 

When I try to load the “Isabelle/src/HOL/Real/Real.thy” to my theory, it reports the following message:

 

***could not find theory file ‘Real.thy” in dir(s) “Real”, ….

***Theory loader: the error(s) above occurred while examining theory “Real”

***At command “theory”.

 

I am using Isabelle2005 in unix platform and my theory content is below:

 

theory FirstTry = “Real/Real”:

end

 

Can anyone teach me how to load an established theory file which is not in the same directory? Thanks in advance.

 

Cheers

Chunqing

 



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