# HG changeset patch
# User traytel
# Date 1531987822 -3600
# Node ID 1e37b45ce3fbc6db823711492f18755a0f72e4c9
# Parent  371e814af6f048d9746d855785d49b4d9c6329bb
normalize imports

diff -r 371e814af6f0 -r 1e37b45ce3fb src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Jul 19 09:10:22 2018 +0100
@@ -8,7 +8,7 @@
 section \<open>Cardinal Arithmetic\<close>
 
 theory Cardinal_Arithmetic
-imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation
+imports Cardinal_Order_Relation
 begin
 
 subsection \<open>Binary sum\<close>
diff -r 371e814af6f0 -r 1e37b45ce3fb src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jul 19 09:10:22 2018 +0100
@@ -8,7 +8,7 @@
 section \<open>Cardinal-Order Relations\<close>
 
 theory Cardinal_Order_Relation
-imports HOL.BNF_Cardinal_Order_Relation Wellorder_Constructions
+imports Wellorder_Constructions
 begin
 
 declare
diff -r 371e814af6f0 -r 1e37b45ce3fb src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Thu Jul 19 09:10:22 2018 +0100
@@ -9,7 +9,7 @@
 
 theory Wellorder_Constructions
 imports
-  HOL.BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
+  Wellorder_Embedding Order_Union
   "HOL-Library.Cardinal_Notations"
 begin
 
diff -r 371e814af6f0 -r 1e37b45ce3fb src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jul 19 09:10:22 2018 +0100
@@ -8,7 +8,7 @@
 section \<open>Well-Order Embeddings\<close>
 
 theory Wellorder_Embedding
-imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation
+imports Fun_More Wellorder_Relation
 begin
 
 subsection \<open>Auxiliaries\<close>
diff -r 371e814af6f0 -r 1e37b45ce3fb src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jul 19 09:10:22 2018 +0100
@@ -8,7 +8,7 @@
 section \<open>Well-Order Relations\<close>
 
 theory Wellorder_Relation
-imports HOL.BNF_Wellorder_Relation Wellfounded_More
+imports Wellfounded_More
 begin
 
 context wo_rel