changeset 16417 | 9bc16273c2d4 |
parent 11456 | 7eb63f63e6c6 |
child 42637 | 381fdcab0f36 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Force = Main: |
2 theory Force imports Main begin |
3 (*Use Divides rather than Main to experiment with the first proof. |
3 (*Use Divides rather than Main to experiment with the first proof. |
4 Otherwise, it is done by the nat_divide_cancel_factor simprocs.*) |
4 Otherwise, it is done by the nat_divide_cancel_factor simprocs.*) |
5 |
5 |
6 declare div_mult_self_is_m [simp del]; |
6 declare div_mult_self_is_m [simp del]; |
7 |
7 |