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