HOL-ex.Coercion_Examples