Email Gateway (Aug 18 2022 at 10:56): Email Gateway (Aug 18 2022 at 10:56):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
HI,
I am just wondering if you know how to load the Complex-Main package
in Isabelle. I have
tried typing:
theory CauchySchwarz
imports Complex_Main
begin
But it says "*** Could not find theory file "Complex_Main.thy" in dir(s)
"/home/s0456778", ".", "$ISABELLE_HOME/src/HOL/Library"
*** Theory loader: the error(s) above occurred while examining theory
"Complex_Main"
*** At command "theory".
Not sure if I am doing something wrong or not but I need to get the
Complex package
working. Also do you know if this package should work off the Bootable
disk, as I could
not get Isabelle to run off my hard drive which is not ideal?
Regards,
Rachel
Email Gateway (Aug 18 2022 at 10:56):From: Tobias Nipkow <nipkow@in.tum.de>
You need to use the HOL-Complex image. Select it in Proof General via
Isabelle -> Logics -> HOL-Complex before you load anything.
(If it is not there yet, you can build it on the shell level via "make
HOL-Complex").
Tobias
RF Todd schrieb:
Last updated: May 03 2024 at 08:18 UTC