| changeset 35123 | e286d5df187a |
| parent 35115 | 446c5063e4fd |
| child 37744 | 3daaf23b9ab4 |
| 35122:305b3eb5b9d5 | 35123:e286d5df187a |
|---|---|
6 signature FLOAT_SYNTAX = |
6 signature FLOAT_SYNTAX = |
7 sig |
7 sig |
8 val setup: theory -> theory |
8 val setup: theory -> theory |
9 end; |
9 end; |
10 |
10 |
11 structure FloatSyntax: FLOAT_SYNTAX = |
11 structure Float_Syntax: FLOAT_SYNTAX = |
12 struct |
12 struct |
13 |
13 |
14 (* parse translation *) |
14 (* parse translation *) |
15 |
15 |
16 local |
16 local |