| changeset 28562 | 4e74209f113e |
| parent 28335 | 25326092cf9a |
| child 28663 | bd8438543bf2 |
| 28561:056255ade52a | 28562:4e74209f113e |
|---|---|
7 |
7 |
8 theory Codegenerator_Pretty |
8 theory Codegenerator_Pretty |
9 imports ExecutableContent Code_Char Efficient_Nat |
9 imports ExecutableContent Code_Char Efficient_Nat |
10 begin |
10 begin |
11 |
11 |
12 declare isnorm.simps [code func del] |
12 declare isnorm.simps [code del] |
13 |
13 |
14 ML {* (*FIXME get rid of this*) |
14 ML {* (*FIXME get rid of this*) |
15 nonfix union; |
15 nonfix union; |
16 nonfix inter; |
16 nonfix inter; |
17 nonfix upto; |
17 nonfix upto; |