From 47b51c85aef5b6f3b6afca5d93698d490744c56d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 7 Oct 1998 16:05:01 +0000 Subject: Added some notes for Isabelle --- INSTALL | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/INSTALL b/INSTALL index 2e2ca7ce..a58ea3b8 100644 --- a/INSTALL +++ b/INSTALL @@ -53,8 +53,8 @@ proof-home so that the autoload directory calculations are correct. ---------------------------------------------------------------------- -Customization for Coq -===================== +Notes for Coq +============= If you want to use this mode for Coq, you need to make sure you have an appropriate version, which is from later than 1 March 1998. @@ -73,8 +73,8 @@ running LEGO, do the same using legotags in the appropriate directory. ---------------------------------------------------------------------- -Customization for LEGO -====================== +Notes for LEGO +============== Install legotags in a standard place or add /lego to your PATH. @@ -83,6 +83,20 @@ NB: You may need to change the path to perl at the top of the file. ---------------------------------------------------------------------- -Customization for Isabelle -========================== +Notes for Isabelle +================== + +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. + +Notice that because Isabelle automatically loads .ML with the same +names as theory files, a sensible way of working with script +management may be to develop your proofs in another file first. +At the moment the interface has no way of knowning that a particular +ML file has been automatically loaded. + + + -- cgit v1.2.3