src/HOL/ex/Coercion_Examples.thy
changeset 54879 a9397557da56
parent 54438 82ef58dba83b
child 55932 68c5104d2204