*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] novice problem about loading theory file*From*: "Chen Chunqing" <g0301019 at nus.edu.sg>*Date*: Fri, 25 Nov 2005 13:58:08 +0800*Thread-index*: AcXxhTWHItmXQh/3RWKFm6+6+Jw4GQ==*Thread-topic*: Re: [isabelle]novice problem about loading theory file

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 = { 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 |

- Previous by Date: Re: [isabelle] novice problem about loading theorey file
- Next by Date: [isabelle] Call for Papers [Reminder]: JAR Special Issue on User Interfaces for Theorem Proving.
- Previous by Thread: [isabelle] Groebner Bases Bibliography
- Next by Thread: [isabelle] Call for Papers [Reminder]: JAR Special Issue on User Interfaces for Theorem Proving.
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list