diff -r 79202e2eab6a -r de49d5780f57 ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Thu Aug 20 14:19:39 2009 +0200
@@ -97,6 +97,7 @@
 fun explicit "" = Default
   | explicit s  = Explicit s
 
+
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean),
   ("linenos", Library.setmp linenos o boolean),