Email Gateway (Aug 18 2022 at 10:07): Email Gateway (Aug 18 2022 at 10:07):From: Paqui Lucio <paqui.lucio@ehu.es>
Hi,
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.
Any suggestion?
Thanks,
Paqui
Paqui Lucio
Dpto de LSI
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20080-San Sebastián
SPAIN
e-mail: paqui.lucio@ehu.es
Tfn: (+34) (9)43 015049
Fax: (+34) (9)43 015590
Web: http://www.sc.ehu.es/paqui
Email Gateway (Aug 18 2022 at 10:13):From: Makarius <makarius@sketis.net>
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?)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC