src/HOL/HOL.thy
changeset 5936 406eb27fe53c
parent 5786 9a2c90bdadfe
child 6027 9dd06eeda95c