src/HOL/HOL.thy
changeset 7333 6cb15c6f1d9f
parent 7238 36e58620ffc8
child 7357 d0e16da40ea2