Email Gateway (Aug 18 2022 at 13:14): Email Gateway (Aug 18 2022 at 13:14):From: Jens Doll <jd@cococo.de>
I am having a problem with the installation instructions. I downloaded the
cygwin Complex_Main and save it to the /usr/local. Then it was tarred with
tar -xzf HOL-*gz. Now Isabelle still says:
*** Could not find theory file "Complex_Main.thy" in ".", "/home/Jens",
"$ISABELLE_HOME/src/HOL/Library"
*** Theory loader: the error(s) above occurred while examining theory
"Complex_Main"
*** At command "theory".
What could be wrong?
Jens
Email Gateway (Aug 18 2022 at 13:15):From: Makarius <makarius@sketis.net>
By "Isabelle" you probably mean your Proof General session. Here you need
to say that you want to use the "HOL-Complex" logic instead of the default
one "HOL".
Makarius
Last updated: May 03 2024 at 12:27 UTC