From 2b6e81b1f4fef8830516a6907dbe8ba8870e7ba1 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 16 Jun 2000 17:10:00 +0000
Subject: proper indentation;

---
 isa/Example.ML | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index 673f7c6f..1fec5c08 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -5,11 +5,11 @@
 *)    
 
 Goal "A & B --> B & A";
-by (rtac impI 1);
-by (etac conjE 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (assume_tac 1);
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
 qed "and_comms";
 
 Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
-- 
cgit v1.2.3