src/HOL/ex/Coercion_Examples.thy
changeset 81512 c1aa8a61ee65
parent 67399 eab6ce8368fa
equal deleted inserted replaced
81511:8cbc8bc6f382 81512:c1aa8a61ee65