# HG changeset patch
# User blanchet
# Date 1347424507 -7200
# Node ID f252c7c2ac7b440a7abbcfab5ba1724c738a3809
# Parent  3f8671b353aea89518a0e09cfd41b1f6775b910a
reduced theory dependencies

diff -r 3f8671b353ae -r f252c7c2ac7b src/HOL/Codatatype/BNF_GFP.thy
--- 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
diff -r 3f8671b353ae -r f252c7c2ac7b src/HOL/Codatatype/BNF_Util.thy
--- 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)"
diff -r 3f8671b353ae -r f252c7c2ac7b src/HOL/Codatatype/Countable_Set.thy
--- 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