1356   also implements a mechanism where a theorem name can refer to a custom theorem 

  1356   also implements a mechanism where a theorem name can refer to a custom theorem 

  1357   list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 

  1357   list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 

  1358   To see how it works let us assume we defined our own theorem list @{text MyThmList}.

  1358   To see how it works let us assume we defined our own theorem list @{text MyThmList}.

  1359 *}

  1359 *}

  1360 

  1360 

  1362   (type T = thm list

  1362   (type T = thm list

  1363    val empty = []

  1363    val empty = []

  1364    val extend = I

  1364    val extend = I

  1366 

  1366 

  1367 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}

  1367 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}

  1368 

  1368 

  1369 text {*

  1369 text {*

  1370   The function @{ML update} allows us to update the theorem list, for example

  1370   The function @{ML update} allows us to update the theorem list, for example