--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Tue Jul 17 12:23:37 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jul 19 09:22:32 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>
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Tue Jul 17 12:23:37 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jul 19 09:22:32 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
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Tue Jul 17 12:23:37 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Thu Jul 19 09:22:32 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
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Tue Jul 17 12:23:37 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Thu Jul 19 09:22:32 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>
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Tue Jul 17 12:23:37 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jul 19 09:22:32 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