src/Doc/System/Misc.thy
changeset 80178 438d583ab378
parent 80158 059d5e115ae3
equal deleted inserted replaced
80169:5e64a54f6790 80178:438d583ab378