src/HOL/SizeChange/Implementation.thy
changeset 27656 d4f6e64ee7cc
parent 27436 9581777503e9
child 28562 4e74209f113e