src/Doc/System/Misc.thy
changeset 71677 ff2c26b8ffb1
parent 71579 9b49538845cc
child 72309 564012e31db1