src/HOL/HOL.thy
changeset 8300 4c3f83414de3
parent 7426 e0be36ee7ab9
child 8473 2798d2f71ec2