| changeset 2747 | a5da7b6aff8f |
| parent 2551 | 26d594a9b89f |
| 2746:6aa98a113e6c | 2747:a5da7b6aff8f |
|---|---|
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 "~~/src/HOL/Library/LaTeXsugar", |
4 "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" ]; |
4 "~~/src/HOL/Quotient_Examples/FSet" ]; |
5 use_thys ["Paper"]; |
5 use_thys ["Paper"]; |