changeset 14269 | 502a7c95de73 |
parent 14268 | 5cf13e80be0e |
child 14270 | 342451d763f9 |
--- a/src/HOL/Real/RealAbs.thy Thu Nov 27 10:47:55 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title : RealAbs.thy - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Absolute value function for the reals -*) - -RealAbs = RealArith