Re: [isabelle] how to import circus after extract circus file for unifying theories



There is no need to combine theories in this way. The theory Main contains everything you need.

I urge you to work through the tutorials. They are the first two items listed on the documentation page 

	http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html

You need to understand the basics before you can try anything advanced.

Larry Paulson


> On 28 Oct 2014, at 17:02, M A <tesleft at hotmail.com> wrote:
> 
> Hi
> 
> expect to unifying theory Lists and Lattices, is lists the correct collection for implementing lattices, if not, which theory for this
> when extract all circus code 
> 
> C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\Designs.thy
> in src directory
> this time error become
> Bad theory (file "C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\Lists.thy")
> 
> theory testlattice
> imports Designs Relations Lists Lattices
> begin
> end
> 
> Regards,
> 
> Martin
> 
> 
> 
>> From: tesleft at hotmail.com
>> To: isabelle-users at cl.cam.ac.uk
>> Date: Wed, 29 Oct 2014 00:55:44 +0800
>> Subject: [isabelle] how to import circus after extract circus file for unifying theories
>> 
>> Hi 
>> 
>> C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\HOL\Circus
>> 
>> Bad theory (file "C:\Users\marin\Downloads\Isabelle\Isabelle2014\src\Circus.thy")
>> 
>> 
>> Regards,
>> 
>> Martin
>> 
>> 
> 
> 		 	   		  





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