symbol syntax for "abs";

--- a/src/HOL/HOL.thy	Sat Nov 18 00:32:08 2000 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 18 19:45:05 2000 +0100
@@ -77,6 +77,11 @@
   inverse       :: "'a::inverse => 'a"
   divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
 
+syntax (xsymbols)
+  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+syntax (HTML output)
+  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+
 axclass plus_ac0 < plus, zero
   commute: "x + y = y + x"
   assoc:   "(x + y) + z = x + (y + z)"