changeset 517 | d8c376662bb4 |
parent 514 | 7e25716c3744 |
child 535 | 5734ab5dd86d |
--- a/ProgTutorial/Package/Ind_Interface.thy Mon Apr 30 12:36:32 2012 +0100 +++ b/ProgTutorial/Package/Ind_Interface.thy Mon Apr 30 14:43:52 2012 +0100 @@ -61,7 +61,7 @@ *} -ML{*val spec_parser = +ML %grayML{*val spec_parser = Parse.fixes -- Scan.optional (Parse.$$$ "where" |-- @@ -177,4 +177,4 @@ introduction rules. The description of this function will span over the next two sections. *} -(*<*)end(*>*) \ No newline at end of file +(*<*)end(*>*)