equal
deleted
inserted
replaced
1714 of Isabelle is completely oblivious about what to do with references, but |
1714 of Isabelle is completely oblivious about what to do with references, but |
1715 properly treats ``data slots''! |
1715 properly treats ``data slots''! |
1716 |
1716 |
1717 Since storing theorems in a list is such a common task, there is the special |
1717 Since storing theorems in a list is such a common task, there is the special |
1718 functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain |
1718 functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain |
1719 a named theorem lists, you just declare |
1719 a named theorem list, you just declare |
1720 *} |
1720 *} |
1721 |
1721 |
1722 ML{*structure FooRules = Named_Thms |
1722 ML{*structure FooRules = Named_Thms |
1723 (val name = "foo" |
1723 (val name = "foo" |
1724 val description = "Rules for foo") *} |
1724 val description = "Rules for foo") *} |