equal
deleted
inserted
replaced
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
2 |
2 |
3 theory HOL4Word32 imports HOL4Base begin |
3 theory HOL4Word32 imports HOL4Base begin |
4 |
4 |
5 ;setup_theory bits |
5 setup_theory "~~/src/HOL/Import/HOL" bits |
6 |
6 |
7 consts |
7 consts |
8 DIV2 :: "nat => nat" |
8 DIV2 :: "nat => nat" |
9 |
9 |
10 defs |
10 defs |
283 ==> (x + (1::nat)) mod n = x mod n + (1::nat)" |
283 ==> (x + (1::nat)) mod n = x mod n + (1::nat)" |
284 by (import bits MOD_ADD_1) |
284 by (import bits MOD_ADD_1) |
285 |
285 |
286 ;end_setup |
286 ;end_setup |
287 |
287 |
288 ;setup_theory word32 |
288 setup_theory "~~/src/HOL/Import/HOL" word32 |
289 |
289 |
290 consts |
290 consts |
291 HB :: "nat" |
291 HB :: "nat" |
292 |
292 |
293 defs |
293 defs |