Re: [isabelle] Pure and CPure non-compatible

On Wed, 31 Jan 2007, Paqui Lucio wrote:

> I would like to import two modules, one is made over Pure and the other 
> is made over Main, but Isabelle system complains that Pure and CPure can 
> not be put together.

I suppose this is Main of Isabelle/HOL not Isabelle/ZF?  Since the 
application syntax of Pure vs. CPure is in conflict, you have to choose 
either branch for your work.  I suggest to adapt the Pure development to 
CPure first.  (What exactly is this anyway?)


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