src/HOL/SizeChange/Implementation.thy
changeset 27123 11fcdd5897dd
parent 26822 67c24cfa8def
child 27436 9581777503e9