# HG changeset patch
# User haftmann
# Date 1330810733 -3600
# Node ID e1569a38448cfb7aecb6d4d4b178c7a16c5348e7
# Parent  f3c10e908f65867b79d5d262d9d0a00d18d752a2
plugged in pre-existing theories appropriately

diff -r f3c10e908f65 -r e1569a38448c src/HOL/Import/HOL4/Generate.thy
--- a/src/HOL/Import/HOL4/Generate.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL4/Generate.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,5 @@
 theory Generate
-imports Compatibility
+imports "Template/GenHOL4Prob" "Template/GenHOL4Vec" "Template/GenHOL4Word32"
 begin
 
 end
diff -r f3c10e908f65 -r e1569a38448c src/HOL/Import/HOL4/Imported.thy
--- a/src/HOL/Import/HOL4/Imported.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL4/Imported.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,6 @@
 theory Imported
-imports Compatibility
+imports "Generated/HOL4Vec" "Generated/HOL4Word32" "Generated/HOL4Real" "Generated/HOL4Prob"
 begin
 
 end
+
diff -r f3c10e908f65 -r e1569a38448c src/HOL/Import/HOL_Light/Generate.thy
--- a/src/HOL/Import/HOL_Light/Generate.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Generate.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,5 @@
 theory Generate
-imports Compatibility
+imports "Template/GenHOLLight"
 begin
 
 end
diff -r f3c10e908f65 -r e1569a38448c src/HOL/Import/HOL_Light/Imported.thy
--- a/src/HOL/Import/HOL_Light/Imported.thy	Sat Mar 03 22:38:33 2012 +0100
+++ b/src/HOL/Import/HOL_Light/Imported.thy	Sat Mar 03 22:38:53 2012 +0100
@@ -1,5 +1,6 @@
 theory Imported
-imports Compatibility
+imports "Generated/HOLLight"
 begin
 
 end
+