[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”:



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





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