src/HOL/HOL.thy
changeset 2355 ee9bdbe2ac8a
parent 2260 b59781f2b809
child 2368 d394336997cf