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 +