HOL-ex.Perm_Fragments