HOL-ex.Specifications_with_bundle_mixins