src/HOL/Library/Accessible_Part.thy
changeset 17076 c7effdf2e2e2
parent 15140 322485b816ac
child 18241 afdba6b3e383