equal
deleted
inserted
replaced
74 |
74 |
75 consts |
75 consts |
76 abs :: "'a::minus => 'a" |
76 abs :: "'a::minus => 'a" |
77 inverse :: "'a::inverse => 'a" |
77 inverse :: "'a::inverse => 'a" |
78 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
78 divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) |
|
79 |
|
80 syntax (xsymbols) |
|
81 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
|
82 syntax (HTML output) |
|
83 abs :: "'a::minus => 'a" ("\<bar>_\<bar>") |
79 |
84 |
80 axclass plus_ac0 < plus, zero |
85 axclass plus_ac0 < plus, zero |
81 commute: "x + y = y + x" |
86 commute: "x + y = y + x" |
82 assoc: "(x + y) + z = x + (y + z)" |
87 assoc: "(x + y) + z = x + (y + z)" |
83 zero: "0 + x = x" |
88 zero: "0 + x = x" |