Isabelle/Isar Proof General has full support for multiple file
scripting, with dependencies between theories communicated between
Isabelle and Proof General.
There is full support for X Symbol, using the Isabelle print mode for
X Symbol tokens. Many Isabelle theories have X Symbol syntax already
defined and it's easy to add to your own theories.
The script `interface' and file 'interface-setup.el' are used
internally to start Isabelle Proof General via the 'Isabelle' shell
command. This is the default way to invoke Proof General from the
Isabelle perspective; it enables Isabelle to provide a consistent
process and file-system environment, including the all-important
isar-keywords.el file.
