src/HOL/ex/Coercion_Examples.thy
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
less more (0) tip