Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] novice problem about loading theory file

view this post on Zulip Email Gateway (Aug 17 2022 at 13:28):

From: Chen Chunqing <g0301019@nus.edu.sg>
Dear all,

Thanks for your help.

I first tried the use the "logic image HOL-Complex rather than HOL" by
starting Isabelle with the command"

Isabelle -l HOL-Complex

And it reports "unkonwn logic "HOL-Complex";

So I follow the other way, i.e., by import the real.thy explicitly by
entering command

imports "~~/src/HOL/Real/Real"

It seems OK with the following message given:

theory FirstTry = {Main, Lubs, Quotient, Rational, PReal, RealDef,
RComplete, RealPow, Real, #}

Hence I suppose that is the right way for me to use real number in
Isabelle, though currently I have not started the proof.

I guess that the reason that the first way fails is that I am using
Isabelle2005 which may have different name for real theory.

Regards

Chunqing

Last updated: May 03 2024 at 04:19 UTC