src/HOL/HOL.thy
changeset 9502 50ec59aff389
parent 9488 f11bece4e2db
child 9529 d9434a9277a4