src/HOL/HOL.thy
changeset 23512 770e7f9f715b
parent 23511 7067f5e3670f
child 23530 438c5d2db482