# HG changeset patch
# User nipkow
# Date 957543846 -7200
# Node ID e3688ef49f12069360e3f9ec4ef4c132de0119c2
# Parent  89e9deef4bcb250a56c98c2fddedfdc2587f92f7
Added constant abs.

diff -r 89e9deef4bcb -r e3688ef49f12 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri May 05 17:49:54 2000 +0200
+++ b/src/HOL/HOL.thy	Fri May 05 18:24:06 2000 +0200
@@ -62,6 +62,7 @@
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
+  abs		:: "('a::minus) => 'a"
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)