| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 03 Jun 2011 12:46:23 +0100 | |
| changeset 2814 | 887d8bd4eb99 |
| parent 2747 | a5da7b6aff8f |
| permissions | -rw-r--r-- |
|
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2471
diff
changeset
|
1 |
no_document use_thys ["../Nominal/Nominal2_Base", |
|
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2471
diff
changeset
|
2 |
"../Nominal/Atoms", |
|
2747
a5da7b6aff8f
precise path to LaTeXsugar
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
3 |
"~~/src/HOL/Library/LaTeXsugar"]; |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
use_thys ["Paper"]; |