--- a/src/HOL/RealDef.thy Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/RealDef.thy Wed Dec 01 20:59:29 2010 +0100
@@ -9,6 +9,7 @@
theory RealDef
imports Rat
+uses "~~/src/Tools/subtyping.ML"
begin
text {*
@@ -1109,6 +1110,11 @@
real_of_nat_def [code_unfold]: "real == real_of_nat"
real_of_int_def [code_unfold]: "real == real_of_int"
+setup Subtyping.setup
+
+declare [[coercion "real::nat\<Rightarrow>real"]]
+declare [[coercion "real::int\<Rightarrow>real"]]
+
lemma real_eq_of_nat: "real = of_nat"
unfolding real_of_nat_def ..