--- 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
+
--- 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
+
--- 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
--- 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
+
--- 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
+
--- 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
+