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/Hyperreal/HyperDef.thy
changeset 12018 ec054019c910
parent 11713 883d559b0b8c
child 13487 1291c6375c29 
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Nov 02 17:55:24 2001 +0100
@@ -30,10 +30,10 @@
 defs
 
   hypreal_zero_def
-  "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})"
+  "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})"
 
   hypreal_one_def
-  "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
+  "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})"
 
   hypreal_minus_def
   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
@@ -43,7 +43,7 @@
 
   hypreal_inverse_def
   "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
-                    hyprel``{%n. if X n = Numeral0 then Numeral0 else inverse (X n)})"
+                    hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
 
   hypreal_divide_def
   "P / Q::hypreal == P * inverse Q"
isabelle