equal
deleted
inserted
replaced
66 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
66 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
67 abs :: "('a::minus) => 'a" |
67 abs :: "('a::minus) => 'a" |
68 * :: "['a::times, 'a] => 'a" (infixl 70) |
68 * :: "['a::times, 'a] => 'a" (infixl 70) |
69 (*See Nat.thy for "^"*) |
69 (*See Nat.thy for "^"*) |
70 |
70 |
|
71 axclass plus_ac0 < plus, zero |
|
72 commute: "x + y = y + x" |
|
73 assoc: "(x + y) + z = x + (y + z)" |
|
74 zero: "0 + x = x" |
71 |
75 |
72 |
76 |
73 (** Additional concrete syntax **) |
77 (** Additional concrete syntax **) |
74 |
78 |
75 nonterminals |
79 nonterminals |