src/HOL/ex/Coercion_Examples.thy
changeset 72611 c7bc3e70a8c7
parent 67399 eab6ce8368fa