src/HOL/HOL.thy
changeset 21234 fb84ab52f23b
parent 21218 38013c3a77a2
child 21250 a268f6288fb6