Re: [isabelle] Receiving error by importing theory file Sum_Of_Squares



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.