| changeset 16417 | 9bc16273c2d4 |
| parent 12815 | 1f073030b97a |
| child 21262 | a2bd14226f9a |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Examples = Main: |
2 theory Examples imports Main begin |
3 |
3 |
4 ML "reset eta_contract" |
4 ML "reset eta_contract" |
5 ML "Pretty.setmargin 64" |
5 ML "Pretty.setmargin 64" |
6 |
6 |
7 text{*membership, intersection *} |
7 text{*membership, intersection *} |