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