1 files changed, 6 insertions, 1 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";