src/Doc/System/Misc.thy
changeset 72428 b7351ffe0dbc
parent 72316 3cc6aa405858
child 72525 8eb0b663fa20