-
Grégoire Lecerf
Joris van der Hoeven
Joris van der Hoeven
mailing-list for TeXmacs Users
Text archives Help
From : Bas Spitters <address@hidden>- To: Paulo Jorge de Oliveira Cantante de Matos <address@hidden>, TeXmacs-users ML <address@hidden>
- Subject: Re: [TeXmacs] Interfacing texmacs with Isabelle
- Date: Thu, 23 Oct 2003 12:58:03 +0200
On Thursday 23 October 2003 13:21, Paulo Jorge de Oliveira Cantante de Matos
wrote:
> Hi all,
>
> Has anyone ever tried to interface texmacs with the Isabelle logical
> framework? I'd like to know if it is even possible, which I'm not sure
> since Isabelle is not a CAS.
Have a look at the work of Phillipe Audebaud for the Coq proof assistant.
http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/
Bas
- Interfacing texmacs with Isabelle, Paulo Jorge de Oliveira Cantante de Matos, 10/23/2003
- Re: [TeXmacs] Interfacing texmacs with Isabelle, Bas Spitters, 10/23/2003
- Re: [TeXmacs] Interfacing texmacs with Isabelle, Joris van der Hoeven, 10/23/2003
- Logical Frameworks [Was: Interfacing texmacs with Isabelle], Andreas Seidl, 10/23/2003
- Re: [TeXmacs] Logical Frameworks [Was: Interfacing texmacs with Isabelle], Joris van der Hoeven, 10/24/2003
- Logical Frameworks [Was: Interfacing texmacs with Isabelle], Andreas Seidl, 10/23/2003
Archive powered by MHonArc 2.6.19.
