src/HOL/HOL.thy
changeset 14722 8e739a6eaf11
parent 14690 f61ea8bfa81e
child 14749 9ccfd0f59e11