src/HOL/HOL.thy
changeset 5204 858da18069d7
parent 5186 439e292b5b87
child 5305 513925de8962