Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Extended_Real.thy
changeset 43924 1165fe965da8
parent 43923 ab93d0190a5d
child 43933 6cc1875cf35d 
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -55,7 +55,7 @@
   instance ..
 end
 
-definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
+definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
 
 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
isabelle