author | wenzelm |
Mon, 28 Aug 2000 14:09:33 +0200 | |
changeset 9697 | c5fc121c2067 |
parent 9429 | 8ebc549e9326 |
child 10715 | c838477b5c18 |
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 |
||
9429 | 8 |
RealAbs = RealArith + |
5078 | 9 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
10 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
11 |
defs |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
12 |
abs_real_def "abs r == (if (#0::real) <= r then r else -r)" |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8856
diff
changeset
|
13 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7334
diff
changeset
|
14 |
end |