From ea3e60264221ccd4bb880f1a30e157b420ca6e66 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Wed, 11 Sep 2002 14:53:10 +0000
Subject: Remove comment about selecting PG/Isar.

---
 isar/Example.thy | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 0d7edca7..fc72c2f7 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,12 +1,7 @@
-(*  -*- isar -*-
-
+(*
       Example proof document for Isabelle/Isar Proof General.
    
       $Id$
-
-      The first line forces Isabelle/Isar Proof General, otherwise
-      you may get the theory mode of ordinary Isabelle Proof General
-      See the manual for other ways to select Isabelle/Isar PG.
 *)
 
 theory Example = Main:
@@ -19,8 +14,9 @@ proof
   then show "B & A"
   proof
     assume B and A
-    then show ?thesis ..
-  qed
+    then
+   show ?thesis ..
+ qed
 qed
 
 
-- 
cgit v1.2.3