52 local |
52 local |
53 |
53 |
54 |
54 |
55 (* Overloaded Constants *) |
55 (* Overloaded Constants *) |
56 |
56 |
57 axclass zero < "term" |
57 axclass zero < "term" |
58 axclass plus < "term" |
58 axclass one < "term" |
|
59 axclass plus < "term" |
59 axclass minus < "term" |
60 axclass minus < "term" |
60 axclass times < "term" |
61 axclass times < "term" |
61 axclass inverse < "term" |
62 axclass inverse < "term" |
62 |
63 |
63 global |
64 global |
64 |
65 |
65 consts |
66 consts |
66 "0" :: "'a::zero" ("0") |
67 "0" :: "'a::zero" ("0") |
|
68 "1" :: "'a::one" ("1") |
67 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
69 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
68 - :: "['a::minus, 'a] => 'a" (infixl 65) |
70 - :: "['a::minus, 'a] => 'a" (infixl 65) |
69 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
71 uminus :: "['a::minus] => 'a" ("- _" [81] 80) |
70 * :: "['a::times, 'a] => 'a" (infixl 70) |
72 * :: "['a::times, 'a] => 'a" (infixl 70) |
|
73 |
|
74 typed_print_translation {* |
|
75 let |
|
76 fun tr' c = (c, fn show_sorts => fn T => fn ts => |
|
77 if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
|
78 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
|
79 in [tr' "0", tr' "1"] end; |
|
80 *} |
71 |
81 |
72 local |
82 local |
73 |
83 |
74 consts |
84 consts |
75 abs :: "'a::minus => 'a" |
85 abs :: "'a::minus => 'a" |