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".
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