symbol syntax for "abs";
authorwenzelm
Sat Nov 18 19:45:05 2000 +0100 (2000-11-18)
changeset 10489a4684cf28edf
parent 10488 adeb9df940b6
child 10490 0054c785f495
symbol syntax for "abs";
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Nov 18 00:32:08 2000 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Nov 18 19:45:05 2000 +0100
     1.3 @@ -77,6 +77,11 @@
     1.4    inverse       :: "'a::inverse => 'a"
     1.5    divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
     1.9 +syntax (HTML output)
    1.10 +  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    1.11 +
    1.12  axclass plus_ac0 < plus, zero
    1.13    commute: "x + y = y + x"
    1.14    assoc:   "(x + y) + z = x + (y + z)"