2223   can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,

  2223   can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,

  2224   let us introduce a theorem list.

  2224   let us introduce a theorem list.

  2225 *}

  2225 *}

  2226 

  2226 

  2227 ML{*structure MyThms = Named_Thms

  2227 ML{*structure MyThms = Named_Thms

  2229    val description = "Theorems for an Attribute") *}

  2229    val description = "Theorems for an Attribute") *}

  2230 

  2230 

  2231 text {* 

  2231 text {* 

  2232   We are going to modify this list by adding and deleting theorems.

  2232   We are going to modify this list by adding and deleting theorems.

  2233   For this we use the two functions @{ML MyThms.add_thm} and

  2233   For this we use the two functions @{ML MyThms.add_thm} and