--- a/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 06:30:35 2012 +0200
+++ b/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 06:35:07 2012 +0200
@@ -8,7 +8,7 @@
header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
theory BNF_GFP
-imports BNF_FP Equiv_Relations_More
+imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Prefix_Order"
keywords
"codata_raw" :: thy_decl and
"codata" :: thy_decl
--- a/src/HOL/Codatatype/BNF_Util.thy Wed Sep 12 06:30:35 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy Wed Sep 12 06:35:07 2012 +0200
@@ -9,9 +9,7 @@
header {* Library for Bounded Natural Functors *}
theory BNF_Util
-imports
- "../Cardinals/Cardinal_Arithmetic"
- "~~/src/HOL/Library/Prefix_Order"
+imports "../Cardinals/Cardinal_Arithmetic"
begin
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
--- a/src/HOL/Codatatype/Countable_Set.thy Wed Sep 12 06:30:35 2012 +0200
+++ b/src/HOL/Codatatype/Countable_Set.thy Wed Sep 12 06:35:07 2012 +0200
@@ -8,7 +8,7 @@
header {* (At Most) Countable Sets *}
theory Countable_Set
-imports "../Cardinal_Arithmetic" "~~/src/HOL/Library/Countable"
+imports "../Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Countable"
begin