*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Receiving error by importing theory file Sum_Of_Squares*From*: charmi panchal <charmipanchal2006 at gmail.com>*Date*: Wed, 4 Apr 2012 10:29:38 +0300

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 ) . Also tried to import this file by writing path of its location in library, but still it didn't work. I am curious about, is there any other appropriate way to import this file ? Thanks, Charmi Panchal

**Follow-Ups**:**Re: [isabelle] Receiving error by importing theory file Sum_Of_Squares***From:*Brian Huffman

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