src/HOL/HOL.thy
changeset 16872 a51699621d22
parent 16775 c1b87ef4a1c3
child 16999 307b2ec590ff