diff -r b4b70d13c995 -r 4dc3baf45d6a src/HOL/ex/Specifications_with_bundle_mixins.thy --- 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 +