*To*: charmi panchal <charmipanchal2006 at gmail.com>*Subject*: Re: [isabelle] Receiving error by importing theory file Sum_Of_Squares*From*: Brian Huffman <huffman at in.tum.de>*Date*: Thu, 5 Apr 2012 10:56:24 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAJqh+_KDQR4CYhHYKnSQbKK6fzQPTmYZc_f66TWAww1n2c=q7A@mail.gmail.com>*References*: <CAJqh+_KDQR4CYhHYKnSQbKK6fzQPTmYZc_f66TWAww1n2c=q7A@mail.gmail.com>

On Wed, Apr 4, 2012 at 9:29 AM, charmi panchal <charmipanchal2006 at gmail.com> wrote: > Hello, > I am trying to import the .thy file " Sum_Of_Squares ", like wise it is > done in one of the Demo files > http://isabelle.in.tum.de/coursematerial/PSV2009-1/session6-2/Demo.thy > > Here I got an error message, it says.. Missing theory (file work folder > location ) . For this theory file to work with Isabelle2011-1, you must modify the header to look exactly like this: theory Demo imports Main "~~/src/HOL/Library/Sum_of_Squares" begin (Note that besides adding the path, you must also change uppercase "Of" to lowercase "of", following a rename of the file.) - Brian

**References**:**[isabelle] Receiving error by importing theory file Sum_Of_Squares***From:*charmi panchal

- Previous by Date: Re: [isabelle] Confusing behavior of a paired set comprehension
- Next by Date: Re: [isabelle] Confusing behavior of a paired set comprehension
- Previous by Thread: [isabelle] Receiving error by importing theory file Sum_Of_Squares
- Next by Thread: [isabelle] Confusing behavior of a paired set comprehension
- Cl-isabelle-users April 2012 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