--- a/ProgTutorial/Base.thy Thu Aug 20 14:19:39 2009 +0200 +++ b/ProgTutorial/Base.thy Thu Aug 20 22:30:20 2009 +0200 @@ -2,7 +2,6 @@ imports Main LaTeXsugar uses "output_tutorial.ML" - "chunks.ML" "antiquote_setup.ML" begin