From 7c9810c7a262715e06a017ad2cedbdf62f4a7a14 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 8 Jun 2000 19:53:12 +0000
Subject: proper indentation;

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

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 7b4fdcac..6abc15e1 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,11 +1,11 @@
 (*  -*- isar -*-
 
-    Example proof document for Isabelle/Isar Proof General.
- 
-    $Id$
+      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
+      The first line forces Isabelle/Isar Proof General, otherwise
+      you may get the theory mode of ordinary Isabelle Proof General
 *)
 
 theory Example = Main:
@@ -13,11 +13,12 @@ theory Example = Main:
 theorem and_comms: "A & B --> B & A"
 proof
   assume "A & B"
-    thus "B & A"
-    proof
-      assume A B
-	show ?thesis 
-	..
-    qed
+  thus "B & A"
+  proof
+    assume A B
+    show ?thesis 
+      ..
+  qed
 qed
+
 end
-- 
cgit v1.2.3