Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Receiving error by importing theory file Sum_O...

Email Gateway (Aug 18 2022 at 19:29):

From: charmi panchal <charmipanchal2006@gmail.com>
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

Last updated: Apr 25 2024 at 01:08 UTC