# HG changeset patch
# User wenzelm
# Date 1567777857 -7200
# Node ID 373d95cf1b9808be13ab224d124e9eba6fded6d2
# Parent  44588e355ca8adde80d1deaef6efd791a1a963fd
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);

diff -r 44588e355ca8 -r 373d95cf1b98 src/HOL/Algebra/Free_Abelian_Groups.thy
--- 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
diff -r 44588e355ca8 -r 373d95cf1b98 src/HOL/ROOT
--- 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 *)