| changeset 41413 | 64cd30d6b0b8 |
| parent 39795 | 9e59b4c11039 |
| child 48611 | b34ff75c23a7 |
| 41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
|---|---|
1 theory Examples imports Main Binomial begin |
1 theory Examples imports Main "~~/src/HOL/Library/Binomial" begin |
2 |
2 |
3 declare [[eta_contract = false]] |
3 declare [[eta_contract = false]] |
4 ML "Pretty.margin_default := 64" |
4 ML "Pretty.margin_default := 64" |
5 |
5 |
6 text{*membership, intersection *} |
6 text{*membership, intersection *} |