src/HOL/HOL.thy
changeset 21318 edb595802d22
parent 21250 a268f6288fb6
child 21404 eb85850d3eb7