equal
deleted
inserted
replaced
1 quick_and_dirty := true; |
1 quick_and_dirty := true; |
2 no_document use_thys ["LaTeXsugar", "../Nominal/NewParser"]; |
2 no_document use_thys ["LaTeXsugar", "../Nominal/Nominal2"]; |
3 use_thys ["Paper"]; |
3 use_thys ["Paper"]; |