author | Christian Urban <urbanc@in.tum.de> |
Fri, 08 Apr 2011 14:23:28 +0800 | |
changeset 2754 | 2a3a37f29f4f |
parent 2748 | 6f38e357b337 |
permissions | -rw-r--r-- |
1484 | 1 |
quick_and_dirty := true; |
2747
a5da7b6aff8f
precise path to LaTeXsugar
Christian Urban <urbanc@in.tum.de>
parents:
2465
diff
changeset
|
2 |
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", |
a5da7b6aff8f
precise path to LaTeXsugar
Christian Urban <urbanc@in.tum.de>
parents:
2465
diff
changeset
|
3 |
"../Nominal/Nominal2"]; |
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
use_thys ["Paper"]; |