equal
deleted
inserted
replaced
60 |
60 |
61 consts |
61 consts |
62 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
62 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
63 - :: "['a::minus, 'a] => 'a" (infixl 65) |
63 - :: "['a::minus, 'a] => 'a" (infixl 65) |
64 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
64 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
|
65 abs :: "('a::minus) => 'a" |
65 * :: "['a::times, 'a] => 'a" (infixl 70) |
66 * :: "['a::times, 'a] => 'a" (infixl 70) |
66 (*See Nat.thy for "^"*) |
67 (*See Nat.thy for "^"*) |
67 |
68 |
68 |
69 |
69 |
70 |