| changeset 1672 | 2c109cd2fdd0 |
| parent 1660 | 8cb42cd97579 |
| child 1674 | 33aff4d854e4 |
| 1671:608196238072 | 1672:2c109cd2fdd0 |
|---|---|
81 |
81 |
82 defs |
82 defs |
83 Unity_def "() == Abs_Unit(True)" |
83 Unity_def "() == Abs_Unit(True)" |
84 |
84 |
85 (* start 8bit 1 *) |
85 (* start 8bit 1 *) |
86 types |
|
87 |
|
88 ('a, 'b) "ò" (infixr 20) |
|
89 |
|
90 translations |
|
91 |
|
92 (type) "x ò y" == (type) "x * y" |
|
93 |
|
94 "³(x,y,zs).b" == "split(³x.³(y,zs).b)" |
|
95 "³(x,y).b" == "split(³x y.b)" |
|
96 |
|
86 (* end 8bit 1 *) |
97 (* end 8bit 1 *) |
87 |
98 |
88 end |
99 end |
89 (*<<<<<<< Prod.thy*) |
100 (*<<<<<<< Prod.thy*) |
90 (* |
101 (* |