author | wenzelm |
Wed, 10 May 2000 22:34:30 +0200 | |
changeset 8856 | 435187ffc64e |
parent 7588 | 26384af93359 |
child 9013 | 9dd0274f76af |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RealAbs.thy |
7219 | 2 |
ID : $Id$ |
5078 | 3 |
Author : Jacques D. Fleuriot |
4 |
Copyright : 1998 University of Cambridge |
|
5 |
Description : Absolute value function for the reals |
|
6 |
*) |
|
7 |
||
8856 | 8 |
RealAbs = RealBin + |
5078 | 9 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7334
diff
changeset
|
10 |
end |