src/HOL/HOL.thy
changeset 5974 6acf3ff0f486
parent 5786 9a2c90bdadfe
child 6027 9dd06eeda95c