Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pure and CPure non-compatible

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: May 03 2024 at 12:27 UTC