1 files changed, 16 insertions, 0 deletions
diff --git a/isa/Example.thy b/isa/Example.thy
new file mode 100644
index 00000000..c43d480f
--- /dev/null
+++ b/isa/Example.thy
@@ -0,0 +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