lib/ProofGeneral/README
author blanchet
Fri Apr 26 12:09:51 2013 +0200 (2013-04-26)
changeset 51790 22517d04d20b
parent 17737 636becdc3ccc
permissions -rw-r--r--
more intuitive syntax for equality-style discriminators of nullary constructors
aspinall@17737
     1
This directory contains a PGIP configuration file "pgip_isar.xml"
aspinall@17737
     2
which can be used to configure the behaviour of PGIP-aware interfaces
aspinall@17737
     3
communicating in PGIP with Isabelle.  The current version of this file
aspinall@17737
     4
is incomplete and experimental, because interfaces that use it are
aspinall@17737
     5
still in development.
aspinall@17737
     6
aspinall@17737
     7
Note that Isabelle does not do anything with the configurations
aspinall@17737
     8
specified here, it simply passes the file directly on to the interface
aspinall@17737
     9
during startup inside an XML message.
aspinall@17737
    10
aspinall@17737
    11
The file which is sent can be overridden at run time by setting the
aspinall@17737
    12
variable ISABELLE_PGIPCONFIG to point to an alternative location.
aspinall@17737
    13
aspinall@17737
    14
The file here is valid wrt to the RELAX compact schema in "pgip.rnc".
aspinall@17737
    15
aspinall@17737
    16
See http://proofgeneral.inf.ed.ac.uk/kit for more details of the
aspinall@17737
    17
Proof General Kit project.
aspinall@17737
    18
aspinall@17737
    19
aspinall@17737
    20
				    -- David Aspinall, Sep 2005.
aspinall@17737
    21