Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
moved coercion decl. for int
authornipkow
Mon, 06 Dec 2010 19:18:02 +0100
changeset 41022 81d337539d57
parent 41021 3efa0ec42ed4
child 41023 9118eb4eb8dc
moved coercion decl. for int
src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions
src/HOL/RealDef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 06 17:33:25 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 06 19:18:02 2010 +0100
@@ -10,7 +10,6 @@
 declare [[coercion_map map]]
 declare [[coercion_map "% f g h . g o h o f"]]
 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
-declare [[coercion int]]
 declare [[coercion "% x . Float x 0"]]
 declare [[coercion "real::float\<Rightarrow>real"]]
 
--- a/src/HOL/RealDef.thy	Mon Dec 06 17:33:25 2010 +0100
+++ b/src/HOL/RealDef.thy	Mon Dec 06 19:18:02 2010 +0100
@@ -1112,6 +1112,7 @@
 declare [[coercion_enabled]]
 declare [[coercion "real::nat\<Rightarrow>real"]]
 declare [[coercion "real::int\<Rightarrow>real"]]
+declare [[coercion "int"]]
 
 lemma real_eq_of_nat: "real = of_nat"
   unfolding real_of_nat_def ..
isabelle