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:
> I am trying to import the .thy file " Sum_Of_Squares ", like wise it is
> done in one of the Demo files
> 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:
imports Main "~~/src/HOL/Library/Sum_of_Squares"
(Note that besides adding the path, you must also change uppercase
"Of" to lowercase "of", following a rename of the file.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and