| author | blanchet |
| Wed, 18 Jul 2012 08:44:04 +0200 | |
| changeset 48308 | 89674e5a4d35 |
| parent 41413 | 64cd30d6b0b8 |
| permissions | -rw-r--r-- |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
15494
diff
changeset
|
1 |
no_document use_thys [ |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
15494
diff
changeset
|
2 |
"~~/src/HOL/Library/LaTeXsugar", |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
15494
diff
changeset
|
3 |
"~~/src/HOL/Library/OptionalSugar" |
|
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
15494
diff
changeset
|
4 |
]; |
| 15337 | 5 |
use_thy "Sugar"; |
6 |