src/HOL/HOL.thy
changeset 12238 09966ccbc84c
parent 12161 ea4fbf26a945
child 12240 0760eda193c4