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