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



Hi 
 
I use Main got error, how to make meet or join in expression of list?
 
Outer syntax error⌂: keyword "=" expected,
but identifier list⌂ was found
 
theory testlattice
imports Main
begin
datatype meetlist list = Nil | Cons meet_commute |
end
 
 
Regards,
 
Martin
 
 
> From: lp15 at cam.ac.uk
> Date: Tue, 28 Oct 2014 17:48:32 +0000
> To: tesleft at hotmail.com
> CC: isabelle-users at cl.cam.ac.uk
> Subject: 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.