tuned;

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";