src/HOL/ex/Specifications_with_bundle_mixins.thy
changeset 73622 4dc3baf45d6a
parent 72739 e7c2848b78e8
child 80723 ac6a69b0f634
--- a/src/HOL/ex/Specifications_with_bundle_mixins.thy	Tue May 04 17:57:16 2021 +0000
+++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy	Wed May 05 16:09:02 2021 +0000
@@ -1,5 +1,5 @@
 theory Specifications_with_bundle_mixins
-  imports "HOL-Library.Perm"
+  imports "HOL-Combinatorics.Perm"
 begin
 
 locale involutory = opening permutation_syntax +