# HG changeset patch
# User wenzelm
# Date 974573105 -3600
# Node ID a4684cf28edf796a00a82a7c250cccdc92318ff9
# Parent  adeb9df940b6fc8c4830a918388384bf92881e20
symbol syntax for "abs";

diff -r adeb9df940b6 -r a4684cf28edf src/HOL/HOL.thy
--- 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)"