diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-12 16:49:15 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-12 16:49:15 +0000 |
| commit | d08b7740b55d4ec337a3f9f8544fe6a91a7dc39a (patch) | |
| tree | 289ac88385cb850ab33321aa2327331e3781f8c6 /INSTALL | |
| parent | 296de38e40b8e6528f0f1adc621c8b99595fc65e (diff) | |
Removed note about probs with update()
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 28 |
1 files changed, 7 insertions, 21 deletions
@@ -10,7 +10,7 @@ Put this line in your emacs file: (load-file "<proofgeneral-home>/generic/proof-site.el") -Where <proofgeneral-home> is replaced by the full path name for +Where <proofgeneral-home> is replaced by the full path name to Proof-General-<something>. The command above will set the Emacs load path and add auto-loads for @@ -28,7 +28,7 @@ notes below, and the file BUGS. If this doesn't help, then contact us via the address below. Proof General maintainer <proofgen@dcs.ed.ac.uk> - School of Computer Science, + LFCS, Division Of Informatics, University of Edinburgh. Edinburgh. @@ -68,11 +68,11 @@ You cannot run more than one instance of Proof General at a time: e.g. if you're using Coq, you won't be able to run LEGO scripts. If there are some assistants supported that you never want to use, -you can remove them from the variable `proof-assistants` in -proof-site.el to prevent Proof General autoloading for files -with particular extensions. This may be useful if you want -to use other modes for those files, for example, you may want -sml-mode for .ML files or Verilog mode for .v files. +you can remove them from the variable `proof-assistants` +to prevent Proof General autoloading for files with particular +extensions. This may be useful if you want to use other modes for +those files, for example, you may want sml-mode for .ML files or +Verilog mode for .v files. The easiest way to do this (and other customization of Proof General) is via the Customize mechanism, see the menu: @@ -135,17 +135,3 @@ Check the value of isabelle-prog-name. The distribution includes a version of Isamode's theory file mode. Use C-h m to check on the features available. -Proof General attempts to lock theory files as well as ML files -when they are loaded. It also attempts to load the theory file -for a .ML file automatically before you start scripting. This -is tricky because Isabelle's theory loader assumes that ML -files are always read together with theory files. At the moment -Proof General uses an altered version of use_thy which doesn't -load the top-level ML file. This can cause confusion in the -theory loader later, especially with update(). To be safe, -try to use just the Proof General interface, and report any -problems to isabelle@dcs.ed.ac.uk. - - - - |