src/HOL/SizeChange/Interpretation.thy
changeset 29270 0eade173f77e
parent 27417 6cc897e2468a
child 30952 7ab2716dd93b