changeset 315 | de49d5780f57 |
parent 311 | ee864694315b |
child 316 | 74f0a06f751f |
--- 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),