new header syntax;

--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -9,7 +9,7 @@
 
 setup_dump "../HOL" "HOL4Base";
 
-append_dump {*theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":*};
+append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};
 
 import_theory bool;
 

--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -9,7 +9,7 @@
 
 setup_dump "../HOL" "HOL4Prob";
 
-append_dump "theory HOL4Prob = HOL4Real:";
+append_dump "theory HOL4Prob imports HOL4Real begin";
 
 import_theory prob_extra;
 

--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -9,7 +9,7 @@
 
 setup_dump "../HOL" "HOL4Real";
 
-append_dump "theory HOL4Real = HOL4Base:";
+append_dump "theory HOL4Real imports HOL4Base begin";
 
 import_theory realax;
 

--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -9,7 +9,7 @@
 
 setup_dump "../HOL" "HOL4Vec";
 
-append_dump "theory HOL4Vec = HOL4Base:";
+append_dump "theory HOL4Vec imports HOL4Base begin";
 
 import_theory res_quan;
 end_import;

--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -9,7 +9,7 @@
 
 setup_dump "../HOL" "HOL4Word32";
 
-append_dump "theory HOL4Word32 = HOL4Base:";
+append_dump "theory HOL4Word32 imports HOL4Base begin";
 
 import_theory bits;
 

--- a/src/HOL/Import/HOL/HOL4Base.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":
+theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
 
 ;setup_theory bool
 

--- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOL4Prob = HOL4Real:
+theory HOL4Prob imports HOL4Real begin
 
 ;setup_theory prob_extra
 

--- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOL4Real = HOL4Base:
+theory HOL4Real imports HOL4Base begin
 
 ;setup_theory realax
 

--- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOL4Vec = HOL4Base:
+theory HOL4Vec imports HOL4Base begin
 
 ;setup_theory res_quan
 

--- a/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 21 17:25:32 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 21 18:04:49 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOL4Word32 = HOL4Base:
+theory HOL4Word32 imports HOL4Base begin
 
 ;setup_theory bits