equal
deleted
inserted
replaced
|
1 (* fixed type for _RE_parsing of strings from frontend |
|
2 WN.11.99, from Markus Wenzel |
|
3 *) |
|
4 |
|
5 Typefix = Script + |
|
6 |
|
7 syntax |
|
8 |
|
9 "_plus" :: 'a |
|
10 "_minus" :: 'a |
|
11 "_umin" :: 'a |
|
12 "_times" :: 'a |
|
13 |
|
14 translations |
|
15 |
|
16 "op +" => "_plus :: [real, real] => real" (*infixl 65 *) |
|
17 "op -" => "_minus :: [real, real] => real" (*infixl 65 *) |
|
18 "uminus"=> "_umin :: [real] => real" (*"- _" [80] 80*) |
|
19 "op *" => "_times :: [real, real] => real" (*infixl 70 *) |
|
20 |
|
21 end |
|
22 |
|
23 |
|
24 ML |
|
25 |
|
26 val parse_translation = |
|
27 [("_plus", curry Term.list_comb (Syntax.const "op +")), |
|
28 ("_minus", curry Term.list_comb (Syntax.const "op -")), |
|
29 ("_umin", curry Term.list_comb (Syntax.const "uminus")), |
|
30 ("_times", curry Term.list_comb (Syntax.const "op *"))]; |