proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
authorwenzelm
Fri, 06 Sep 2019 15:50:57 +0200
changeset 70850 373d95cf1b98
parent 70849 44588e355ca8
child 70851 9c4809ec28ef
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
src/HOL/Algebra/Free_Abelian_Groups.thy
src/HOL/ROOT
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Sep 06 15:45:05 2019 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Sep 06 15:50:57 2019 +0200
@@ -2,7 +2,7 @@
 
 theory Free_Abelian_Groups
   imports
-    Product_Groups "../Cardinals/Cardinal_Arithmetic"
+    Product_Groups "HOL-Cardinals.Cardinal_Arithmetic"
    "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence"
 
 begin
--- a/src/HOL/ROOT	Fri Sep 06 15:45:05 2019 +0200
+++ b/src/HOL/ROOT	Fri Sep 06 15:50:57 2019 +0200
@@ -326,6 +326,8 @@
 
     The Isabelle Algebraic Library.
   "
+  sessions
+    "HOL-Cardinals"
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)