aboutsummaryrefslogtreecommitdiff
path: root/isa/Example.thy
diff options
context:
space:
mode:
authorDavid Aspinall2002-09-11 14:53:20 +0000
committerDavid Aspinall2002-09-11 14:53:20 +0000
commit879c174f584069404737db54eb0527e2f142f7c1 (patch)
tree3e18b3b9c26e0187fbd68dfff75955ddb48973c6 /isa/Example.thy
parentea3e60264221ccd4bb880f1a30e157b420ca6e66 (diff)
Adjust comment about selecting PG/Isar.
Diffstat (limited to 'isa/Example.thy')
-rw-r--r--isa/Example.thy6
1 files changed, 5 insertions, 1 deletions
diff --git a/isa/Example.thy b/isa/Example.thy
index c43d480f..ba64d959 100644
--- a/isa/Example.thy
+++ b/isa/Example.thy
@@ -10,7 +10,11 @@
Proof General's classic Isabelle mode;
scripting takes place in .ML files.
- NB: this is incompatible with PG/Isar.
+ NB: this is incompatible with ProofGeneral/Isar which is
+ a separate instance of Proof General.
+
+ See the PG manual for ways to select Isabelle/Classic
+ by default.
*)
Example = Main