Creating a clear interface to add and remove thms from the thmsetdata.

[ordinarymath]

Currently the thmsetdata api provides functions for api users to define. This has resulted in very inconsistent naming. One such example would be to add a theorem FOO to [compute] and [simp], you would have to use these two functions.

val _ = BasicProvers.export_rewrites ["FOO"]
val _ = computeLib.add_persistent_funs ["FOO"]

This issue is about depreciating usage of such functions and writing a clean user interface to add, remove and delete theorems.

[mn200]

This can almost be implemented as

fun remove_from_set {settype,thmname} = 
  #remove $ valOf $ ThmSetData.data_exportfns {settype=settype} thmname
fun add_to_set{settype,thmname,thm} = 
  #add $ valOf $ ThmSetData.data_exportfns {settype=settype} (thmname, thm)

but the types of the add and remove fields are not quite right for exactly this.