src/HOL/ex/Coercion_Examples.thy
changeset 55147 bce3dbc11f95
parent 54438 82ef58dba83b
child 55932 68c5104d2204
equal deleted inserted replaced
55146:525309c2e4ee 55147:bce3dbc11f95