Added constant abs.
authornipkow
Fri May 05 18:24:06 2000 +0200 (2000-05-05)
changeset 8800e3688ef49f12
parent 8799 89e9deef4bcb
child 8801 9d01c9a26134
Added constant abs.
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Fri May 05 17:49:54 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri May 05 18:24:06 2000 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
     1.5    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
     1.6    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
     1.7 +  abs		:: "('a::minus) => 'a"
     1.8    *             :: "['a::times, 'a] => 'a"          (infixl 70)
     1.9    (*See Nat.thy for "^"*)
    1.10