changeset 51247 | 064683ba110c |
parent 40839 | 48e01d16dd17 |
child 51320 | c1cb872ccb2b |
--- a/src/HOL/ex/Coercion_Examples.thy Fri Feb 22 13:36:31 2013 +0100 +++ b/src/HOL/ex/Coercion_Examples.thy Fri Feb 22 13:38:10 2013 +0100 @@ -5,9 +5,11 @@ *) theory Coercion_Examples -imports Complex_Main +imports Main begin +declare[[coercion_enabled]] + (* Error messages test *) consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"