Ticket #487 (new feature)

Opened 21 months ago

Last modified 13 months ago

integrate Isabelle as a full logic node (also read in theories)

Reported by: till Owned by: maeder
Priority: critical Milestone: 0.95
Component: provers Version: 0.8
Keywords: Cc:

Description

Use the XML output of Isabelle to read in Isabelle theories into Hets (and thus also make them available for specification in HasCASL).

It may be useful to rely on a connection between Isabelle and OMDoc.

Change History

Changed 16 months ago by luecke

  • milestone changed from 0.9 to 0.93

Changed 13 months ago by maeder

Which XML output of Isabelle (I'm asking cl-isabelle-users@…)?

Changed 13 months ago by maeder

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-October/msg00052.html looks like a lot of work

Note: See TracTickets for help on using tickets.