src/HOL/HOL.thy
changeset 8657 b9475dad85ed
parent 8640 2f9b008a27a1
child 8800 e3688ef49f12