ProgTutorial/FirstSteps.thy
changeset 281 32b4d3704415
parent 280 a63ca3a9b44a
child 282 bfcb8edbd851
equal deleted inserted replaced
280:a63ca3a9b44a 281:32b4d3704415
  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") *}