# HG changeset patch
# User haftmann
# Date 1330804883 -3600
# Node ID 3e89a5cab8d778a24f459935b6a788eedc6c678c
# Parent  d50855d9ea74f5f318088969e8caf496dc7902af
tuned whitespace

diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Import/HOL/HOL4.thy
--- a/src/HOL/Import/HOL/HOL4.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -2,6 +2,9 @@
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
-theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin
+theory HOL4
+imports HOL4Vec HOL4Word32 HOL4Real
+begin
 
 end
+
diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Import/HOL4Setup.thy
--- a/src/HOL/Import/HOL4Setup.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Import/HOL4Setup.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -166,3 +166,4 @@
 setup Import.setup
 
 end
+
diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Import/HOL4Syntax.thy
--- a/src/HOL/Import/HOL4Syntax.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Import/HOL4Syntax.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -9,4 +9,4 @@
 
 ML {* HOL4ImportSyntax.setup() *}
 
-end
\ No newline at end of file
+end
diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Import/HOLLightInt.thy
--- a/src/HOL/Import/HOLLightInt.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Import/HOLLightInt.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -205,3 +205,4 @@
   by (auto simp add: crossproduct_eq)
 
 end
+
diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Import/HOLLightReal.thy
--- a/src/HOL/Import/HOLLightReal.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Import/HOLLightReal.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -326,3 +326,4 @@
   by (simp add: ext)
 
 end
+
diff -r d50855d9ea74 -r 3e89a5cab8d7 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat Mar 03 21:00:31 2012 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Mar 03 21:01:23 2012 +0100
@@ -589,3 +589,4 @@
   by (simp add: atmost_one_def)
 
 end
+