# HG changeset patch
# User wenzelm
# Date 1127318689 -7200
# Node ID 484ff733f29ce8d265257d030f12498bcb1d912c
# Parent  7322f37d334473f9b19c2c1a8369aa0314ad6ce9
new header syntax;

diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- 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;
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
--- 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;
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- 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;
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
--- 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;
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
--- 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;
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/HOL/HOL4Base.thy
--- 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
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/HOL/HOL4Prob.thy
--- 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
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/HOL/HOL4Real.thy
--- 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
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/HOL/HOL4Vec.thy
--- 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
 
diff -r 7322f37d3344 -r 484ff733f29c src/HOL/Import/HOL/HOL4Word32.thy
--- 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