src/HOL/ex/Coercion_Examples.thy
changeset 51317 0e70cc4e94e8
parent 51247 064683ba110c
child 51320 c1cb872ccb2b