src/HOL/SizeChange/Implementation.thy
changeset 27885 76b51cd0a37c
parent 27436 9581777503e9
child 28562 4e74209f113e