equal
deleted
inserted
replaced
1 no_document use_thy "../Myhill"; |
|
2 no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; |
|
3 no_document use_thy "../Derivs"; |
|
4 no_document use_thy "../Closure"; |
1 no_document use_thy "../Closure"; |
5 |
2 |
6 use_thy "Paper" |
3 use_thy "Paper" |