src/HOL/HOL.thy
changeset 14215 ebf291f3b449
parent 14208 144f45277d5a
child 14223 0ee05eef881b