# HG changeset patch
# User blanchet
# Date 1346167199 -7200
# Node ID b62d14275b89370cec4055e0c39f0613a1ebd42c
# Parent  dcb486124b6a94839158a41b5329fbad324ff41c
fixed import paths

diff -r dcb486124b6a -r b62d14275b89 src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,10 +8,8 @@
 header {* Library for Bounded Natural Functors *}
 
 theory BNF_Library
-imports
-   "../Ordinals_and_Cardinals_Base/Cardinal_Arithmetic"
-   "~~/src/HOL/Library/List_Prefix"
-   Equiv_Relations_More
+imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/List_Prefix"
+  Equiv_Relations_More
 begin
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Codatatype/Basic_BNFs.thy
--- a/src/HOL/Codatatype/Basic_BNFs.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -10,8 +10,7 @@
 header {* Registration of Various Types as Bounded Natural Functors *}
 
 theory Basic_BNFs
-imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet"
-        "~~/src/HOL/Library/Multiset" Countable_Set
+imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/Multiset" Countable_Set
 begin
 
 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Codatatype/Countable_Set.thy
--- a/src/HOL/Codatatype/Countable_Set.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Codatatype/Countable_Set.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,8 +8,7 @@
 header {* (At Most) Countable Sets *}
 
 theory Countable_Set
-imports "../Ordinals_and_Cardinals_Base/Cardinal_Arithmetic"
-        "~~/src/HOL/Library/Countable"
+imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Countable"
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Ordinals_and_Cardinals/Cardinal_Order_Relation.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Cardinal_Order_Relation.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,9 +8,7 @@
 header {* Cardinal-Order Relations *}
 
 theory Cardinal_Order_Relation
-imports
-  "../Ordinals_and_Cardinals_Base/Cardinal_Order_Relation_Base"
-  Constructions_on_Wellorders
+imports Cardinal_Order_Relation_Base Constructions_on_Wellorders
 begin
 
 declare
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Ordinals_and_Cardinals/Constructions_on_Wellorders.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Constructions_on_Wellorders.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,9 +8,7 @@
 header {* Constructions on Wellorders *}
 
 theory Constructions_on_Wellorders
-imports
-  "../Ordinals_and_Cardinals_Base/Constructions_on_Wellorders_Base"
-  Wellorder_Embedding
+imports Constructions_on_Wellorders_Base Wellorder_Embedding
 begin
 
 declare
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Fun_More.thy
--- a/src/HOL/Ordinals_and_Cardinals/Fun_More.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Fun_More.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,7 +8,7 @@
 header {* More on Injections, Bijections and Inverses *}
 
 theory Fun_More
-imports "../Ordinals_and_Cardinals_Base/Fun_More_Base"
+imports Fun_More_Base
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Order_Relation_More.thy
--- a/src/HOL/Ordinals_and_Cardinals/Order_Relation_More.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Order_Relation_More.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,7 +8,7 @@
 header {* Basics on Order-Like Relations *}
 
 theory Order_Relation_More
-imports "../Ordinals_and_Cardinals_Base/Order_Relation_More_Base"
+imports Order_Relation_More_Base
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Wellfounded_More.thy
--- a/src/HOL/Ordinals_and_Cardinals/Wellfounded_More.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Wellfounded_More.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,9 +8,7 @@
 header {* More on Well-Founded Relations *}
 
 theory Wellfounded_More
-imports
-  "../Ordinals_and_Cardinals/Wellfounded_More_Base"
-  Order_Relation_More
+imports Wellfounded_More_Base Order_Relation_More
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,10 +8,7 @@
 header {* Well-Order Embeddings *}
 
 theory Wellorder_Embedding
-imports
-  "../Ordinals_and_Cardinals_Base/Wellorder_Embedding_Base"
-  Fun_More
-  Wellorder_Relation
+imports "../Ordinals_and_Cardinals_Base/Wellorder_Embedding_Base" Fun_More Wellorder_Relation
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy
--- a/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding_Base.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,10 +8,7 @@
 header {* Well-Order Embeddings (Base) *}
 
 theory Wellorder_Embedding_Base
-imports
-  "~~/src/HOL/Library/Zorn"
-  Fun_More_Base
-  Wellorder_Relation_Base
+imports "~~/src/HOL/Library/Zorn" Fun_More_Base Wellorder_Relation_Base
 begin
 
 
diff -r dcb486124b6a -r b62d14275b89 src/HOL/Ordinals_and_Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Ordinals_and_Cardinals/Wellorder_Relation.thy	Tue Aug 28 17:17:41 2012 +0200
+++ b/src/HOL/Ordinals_and_Cardinals/Wellorder_Relation.thy	Tue Aug 28 17:19:59 2012 +0200
@@ -8,9 +8,7 @@
 header {* Well-Order Relations *}
 
 theory Wellorder_Relation
-imports
-  "../Ordinals_and_Cardinals_Base/Wellorder_Relation_Base"
-  Wellfounded_More
+imports Wellorder_Relation_Base Wellfounded_More
 begin