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.