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



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.