normalize imports
authortraytel
Thu, 19 Jul 2018 09:10:22 +0100
changeset 68649 1e37b45ce3fb
parent 68648 371e814af6f0
child 68654 5a5146c3a35b
normalize imports
src/HOL/Cardinals/Cardinal_Arithmetic.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Wellorder_Constructions.thy
src/HOL/Cardinals/Wellorder_Embedding.thy
src/HOL/Cardinals/Wellorder_Relation.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>
--- 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
--- 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
 
--- 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>
--- 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