extend_basic_convs : string * (term * conv) -> unit
extend_basic_convs("name",(`pat`,conv))
# REWRITE_CONV[] `x = 1 + 2 + 3 + 4`;; val it : thm = |- x = 1 + 2 + 3 + 4 <=> x = 1 + 2 + 3 + 4
# extend_basic_convs("addition on nat",(`m + n:num`,NUM_ADD_CONV));; val it : unit = ()
# REWRITE_CONV[] `x = 1 + 2 + 3 + 4`;; val it : thm = |- x = 1 + 2 + 3 + 4 <=> x = 10