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/Real/RealAbs.thy
changeset 14265 95b42e69436c
parent 12018 ec054019c910 
--- a/src/HOL/Real/RealAbs.thy	Thu Nov 20 10:42:00 2003 +0100
+++ b/src/HOL/Real/RealAbs.thy	Fri Nov 21 11:15:40 2003 +0100
@@ -5,10 +5,4 @@
     Description : Absolute value function for the reals
 *) 
 
-RealAbs = RealArith +
-
-
-defs
-  real_abs_def "abs r == (if (0::real) <= r then r else -r)"
-
-end
+RealAbs = RealArith
isabelle