src/HOL/HOL.thy
changeset 10489 a4684cf28edf
parent 10432 3dfbc913d184
child 11432 8a203ae6efe3
     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)"