| changeset 40283 | 805ce1d64af0 |
| parent 40282 | 329cd9dd5949 |
| child 40297 | c753e3f8b4d6 |
--- a/src/HOL/ex/Coercion_Examples.thy Fri Oct 29 21:49:33 2010 +0200 +++ b/src/HOL/ex/Coercion_Examples.thy Fri Oct 29 22:07:48 2010 +0200 @@ -9,6 +9,8 @@ uses "~~/src/Tools/subtyping.ML" begin +setup Subtyping.setup + (* Coercion/type maps definitions*) consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"