equal
deleted
inserted
replaced
1 no_document use_thys ["../Nominal/Nominal2_Base", |
1 no_document use_thys ["../Nominal/Nominal2_Base", |
2 "../Nominal/Atoms", |
2 "../Nominal/Atoms", |
3 "LaTeXsugar"]; |
3 "~~/src/HOL/Library/LaTeXsugar"]; |
4 |
4 |
5 use_thys ["Paper"]; |
5 use_thys ["Paper"]; |