| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 17 Dec 2011 16:36:51 +0000 | |
| branch | Nominal2-Isabelle2011-1 |
| changeset 3067 | c32bdb3f0a68 |
| parent 2747 | a5da7b6aff8f |
| permissions | -rw-r--r-- |
|
2368
d7dfe272b4f8
some test with quotient
Christian Urban <urbanc@in.tum.de>
parents:
2186
diff
changeset
|
1 |
quick_and_dirty := true; |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
no_document use_thys ["Quotient", |
|
2747
a5da7b6aff8f
precise path to LaTeXsugar
Christian Urban <urbanc@in.tum.de>
parents:
2551
diff
changeset
|
3 |
"~~/src/HOL/Library/LaTeXsugar", |
|
a5da7b6aff8f
precise path to LaTeXsugar
Christian Urban <urbanc@in.tum.de>
parents:
2551
diff
changeset
|
4 |
"~~/src/HOL/Quotient_Examples/FSet" ]; |
|
2551
26d594a9b89f
FSet changes for Qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2368
diff
changeset
|
5 |
use_thys ["Paper"]; |