From f2e7d83e6c2a68cc07b27332fc9cc7ef07400869 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 2 Aug 2000 15:34:38 +0000
Subject: tuned;

---
 isa/Example2.ML | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'isa/Example2.ML')

diff --git a/isa/Example2.ML b/isa/Example2.ML
index 5d904930..ab2fef03 100644
--- a/isa/Example2.ML
+++ b/isa/Example2.ML
@@ -4,12 +4,12 @@
     $Id$
 
     Same as Example.ML, except using X-Symbol input tokens.
-*)    
+*)
 
 Goal "A \\<and> B \\<longrightarrow> B \\<and> 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";
-- 
cgit v1.2.3