author | griff |
Wed, 22 Jul 2009 09:21:21 +0200 | |
changeset 281 | 32b4d3704415 |
parent 280 | a63ca3a9b44a |
child 282 | bfcb8edbd851 |
ProgTutorial/FirstSteps.thy | file | annotate | diff | comparison | revisions | |
progtutorial.pdf | file | annotate | diff | comparison | revisions |
--- a/ProgTutorial/FirstSteps.thy Wed Jul 22 08:54:24 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Wed Jul 22 09:21:21 2009 +0200 @@ -1716,7 +1716,7 @@ Since storing theorems in a list is such a common task, there is the special functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain - a named theorem lists, you just declare + a named theorem list, you just declare *} ML{*structure FooRules = Named_Thms