From 72b2ab5a832f64c9bd93e6fb26c704029fa0c982 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 24 Jun 2002 09:06:17 +0000
Subject: Add Emacs mode comments at top

---
 isa/Example.ML  | 7 ++++++-
 isa/Example.thy | 8 +++++++-
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/isa/Example.ML b/isa/Example.ML
index 720e3a47..57733a48 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -1,7 +1,12 @@
-(*
+(*  -*- isa -*-
+
     Example proof script for Isabelle Proof General.
 
     $Id$
+
+    The line at the top of this comment forces 
+    Proof General's classic Isabelle mode
+    (instead of Isar: you can't use both at once).
 *)
 
 Goal "A & B --> B & A";
diff --git a/isa/Example.thy b/isa/Example.thy
index 252a5a4c..c43d480f 100644
--- a/isa/Example.thy
+++ b/isa/Example.thy
@@ -1,10 +1,16 @@
-(*
+(*  -*- isa -*- 
+
     Example theory file for Isabelle
 
     David Aspinall <da@dcs.ed.ac.uk>
 
     $Id$
 
+    The line at the top of this comment forces 
+    Proof General's classic Isabelle mode;
+    scripting takes place in .ML files.
+
+    NB: this is incompatible with PG/Isar.
 *)
 
 Example = Main
-- 
cgit v1.2.3