src/HOL/ex/Coercion_Examples.thy
changeset 73475 4840ce456b4f
parent 67399 eab6ce8368fa
equal deleted inserted replaced
73474:4e12a6caefb3 73475:4840ce456b4f