src/HOL/ex/Coercion_Examples.thy
changeset 70923 98d9b78b7f47
parent 67399 eab6ce8368fa