src/HOL/HOL.thy
changeset 15506 864238c95b56
parent 15481 fc075ae929e4
child 15524 2ef571f80a55