*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] novice problem about loading theorey file*From*: "Chen Chunqing" <g0301019 at nus.edu.sg>*Date*: Thu, 24 Nov 2005 11:44:03 +0800*Thread-index*: AcXwqVACLBA6SJEhSvq/yRcp1hKCCw==*Thread-topic*: novice problem about loading theorey file

Dear all, When I try to load the “Isabelle/src/HOL/Real/Real.thy” to
my theory, it reports the following message: ***could not find theory file ‘Real.thy” in dir(s) “Real”, ….
***Theory loader: the error(s) above occurred while examining
theory “Real” ***At command “theory”. I am using Isabelle2005 in unix platform and my theory content
is below: theory FirstTry = “Real/Real”: … end Can anyone teach me how to load an established theory file
which is not in the same directory? Thanks in advance. Cheers Chunqing |

**Follow-Ups**:**Re: [isabelle] novice problem about loading theorey file***From:*Lawrence Paulson

**Re: [isabelle] novice problem about loading theorey file***From:*Jeremy Dawson

**Re: [isabelle] novice problem about loading theorey file***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] Creating new Isar theorem attributes
- Next by Date: Re: [isabelle] novice problem about loading theorey file
- Previous by Thread: Re: [isabelle] Creating new Isar theorem attributes
- Next by Thread: Re: [isabelle] novice problem about loading theorey file
- 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