Opened 17 years ago
Last modified 11 years ago
#144 new enhancement
Build a hybrid top level that removes PG specific one
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
The hybrid top level can use special tokens to recognise PGIP input using XML headers =<?xml ...>=. For this the =xml.ML= module needs to be improved.
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.0.7 deleted