| author | paulson |
| Fri, 21 Nov 2003 11:15:40 +0100 | |
| changeset 14265 | 95b42e69436c |
| parent 12018 | ec054019c910 |
| permissions | -rw-r--r-- |
| paulson@5078 | 1 |
(* Title : RealAbs.thy |
| paulson@7219 | 2 |
ID : $Id$ |
| paulson@5078 | 3 |
Author : Jacques D. Fleuriot |
| paulson@5078 | 4 |
Copyright : 1998 University of Cambridge |
| paulson@5078 | 5 |
Description : Absolute value function for the reals |
| paulson@5078 | 6 |
*) |
| paulson@5078 | 7 |
|
| paulson@14265 | 8 |
RealAbs = RealArith |