src/HOL/ex/Coercion_Examples.thy
changeset 52900 d29bf6db8a2d
parent 51335 6bac04a6a197
child 54438 82ef58dba83b