src/Doc/System/Misc.thy
changeset 59046 db5a718e8c09
parent 58618 782f0b662cae
child 61406 eb2463fc4d7b