Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
authorwenzelm
Fri, 06 Sep 2019 15:50:57 +0200
changeset 70660 373d95cf1b98
parent 70659 44588e355ca8
child 70661 9c4809ec28ef
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
src/HOL/Algebra/Free_Abelian_Groups.thy file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle