src/HOL/HOL.thy
changeset 14421 ee97b6463cb4
parent 14398 c5c47703f763
child 14430 5cb24165a2e1