equal
deleted
inserted
replaced
68 power < term |
68 power < term |
69 |
69 |
70 consts |
70 consts |
71 "+" :: ['a::plus, 'a] => 'a (infixl 65) |
71 "+" :: ['a::plus, 'a] => 'a (infixl 65) |
72 "-" :: ['a::minus, 'a] => 'a (infixl 65) |
72 "-" :: ['a::minus, 'a] => 'a (infixl 65) |
73 uminus :: ['a::minus] => 'a ("- _" [71] 70) |
73 uminus :: ['a::minus] => 'a ("- _" [81] 80) |
74 "*" :: ['a::times, 'a] => 'a (infixl 70) |
74 "*" :: ['a::times, 'a] => 'a (infixl 70) |
75 (*See Nat.thy for "^"*) |
75 (*See Nat.thy for "^"*) |
76 |
76 |
77 |
77 |
78 (** Additional concrete syntax **) |
78 (** Additional concrete syntax **) |