Re: [isabelle] novice problem about loading theorey file



The theories of the reals, complex numbers, etc., are available preloaded. You have to do two things:

* Base your theory upon the theory Complex_Main.
* Use the logic image HOL-Complex rather than HOL, e.g. via the command "Isabelle -l HOL-Complex".

Larry Paulson


On 24 Nov 2005, at 03:44, Chen Chunqing wrote:

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.