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

---
 isa/Example.ML  |  8 +++-----
 isa/Example.thy |  4 ++--
 isa/Example2.ML | 12 ++++++------
 3 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/isa/Example.ML b/isa/Example.ML
index 49b6ee5a..4795d79f 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -2,7 +2,7 @@
     Example proof script for Isabelle Proof General.
 
     $Id$
-*)    
+*)
 
 Goal "A & B --> B & A";
   by (rtac impI 1);
@@ -13,7 +13,5 @@ Goal "A & B --> B & A";
 qed "and_comms";
 
 Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
-by (blast_tac (claset()) 1);
-
-
-
+  by (blast_tac (claset()) 1);
+qed "";
diff --git a/isa/Example.thy b/isa/Example.thy
index 84a71f31..252a5a4c 100644
--- a/isa/Example.thy
+++ b/isa/Example.thy
@@ -1,10 +1,10 @@
 (*
-    Example theory file for Isabelle  
+    Example theory file for Isabelle
 
     David Aspinall <da@dcs.ed.ac.uk>
 
     $Id$
 
-*)    
+*)
 
 Example = Main
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