| changeset 2551 | 26d594a9b89f |
| parent 2368 | d7dfe272b4f8 |
| child 2747 | a5da7b6aff8f |
| 2550:551c5a8b6b2c | 2551:26d594a9b89f |
|---|---|
1 quick_and_dirty := true; |
1 quick_and_dirty := true; |
2 no_document use_thys ["Quotient", |
2 no_document use_thys ["Quotient", |
3 "LaTeXsugar", |
3 "LaTeXsugar", |
4 "../Nominal/FSet" ]; |
4 "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ]; |
5 |
|
6 use_thys ["Paper"]; |
5 use_thys ["Paper"]; |