author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Tue, 19 Feb 2013 05:38:46 +0000 | |
branch | Nominal2-Isabelle2013 |
changeset 3206 | fb201e383f1b |
parent 2985 | 05ccb61aa628 |
permissions | -rw-r--r-- |
2985
05ccb61aa628
started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
quick_and_dirty := true; |
05ccb61aa628
started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", |
05ccb61aa628
started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
"../Nominal/Nominal2"]; |
05ccb61aa628
started lmcs paper (isabelle make lmcs)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
use_thys ["Paper"]; |