changeset 17566 | 484ff733f29c |
parent 17188 | a26a4fc323ed |
child 17644 | bd59bfd4bf37 |
17565:7322f37d3344 | 17566:484ff733f29c |
---|---|
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
2 |
2 |
3 theory HOL4Word32 = HOL4Base: |
3 theory HOL4Word32 imports HOL4Base begin |
4 |
4 |
5 ;setup_theory bits |
5 ;setup_theory bits |
6 |
6 |
7 consts |
7 consts |
8 DIV2 :: "nat => nat" |
8 DIV2 :: "nat => nat" |