src/HOL/HOL.thy
changeset 26875 e18574413bc4
parent 26747 f32fa5f5bdd1
child 26957 e3f04fdd994d