changeset 16417 | 9bc16273c2d4 |
parent 15647 | b1f486a9c56b |
child 17188 | a26a4fc323ed |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
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" |