changeset 2465 | 07ffa4e41659 |
parent 2330 | 8728f7990f6d |
child 2747 | a5da7b6aff8f |
--- a/Paper/ROOT.ML Fri Sep 03 22:22:43 2010 +0800 +++ b/Paper/ROOT.ML Fri Sep 03 22:35:35 2010 +0800 @@ -1,3 +1,3 @@ quick_and_dirty := true; -no_document use_thys ["LaTeXsugar", "../Nominal/NewParser"]; +no_document use_thys ["LaTeXsugar", "../Nominal/Nominal2"]; use_thys ["Paper"]; \ No newline at end of file