diff options
| author | David Aspinall | 1999-11-25 15:13:52 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-25 15:13:52 +0000 |
| commit | 5758742b835d8b3012c086538d57aa590b788dda (patch) | |
| tree | 530e86a2d70661a4db5b1c006b1076458e339cad | |
| parent | 9f6039b8920a88245ddaef45461064860c7f4432 (diff) | |
Added note about non-proof .ML files.
| -rw-r--r-- | doc/ProofGeneral.texi | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index d52d9edf..5d099e30 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2730,10 +2730,12 @@ Note that in ``classic'' Isabelle, @file{.thy} files contain definitions and declarations for a theory, while @file{.ML} contain proof scripts. So most of Proof General's functions only make sense in @file{.ML} files, and there is no toolbar and only a short menu for @file{.thy} -files. +files. Also note that Proof General does not understand full ML +syntax(!), so you should only use the scripting commands on @file{.ML} +files which contain proof commands (no ML functions, structures, etc). There is no specific documentation here for the Isabelle/Isar instance -of Proof General. It is quite With Isar, @file{.thy} files contain proofs as well +of Proof General. With Isar, @file{.thy} files contain proofs as well as theory definitions, and so they support the toolbar and usual scripting functions of Proof General. To load the Isabelle/Isar instance of Proof General, you can set |