From e36ec50c0995858321748f5d4f7bd73472e2464d Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Wed, 16 Jan 2002 16:39:06 +0000
Subject: Whitespace

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

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 357fa09e..4cf33e0b 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -40,8 +40,10 @@ theorem "A & B --> B & A"
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
-   apply assumption
   apply assumption
-  done
+  apply assumption
+done
 
 end
+
+(* comment at the end *)
-- 
cgit v1.2.3