--- 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)"
--- 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]
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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