:makelemma now works on provisional definitions

Adding an appropriate pattern matching definition after the provisional
line. e.g. on foo_lemma in:

foo x y ?= {foo_lemma} z

it will generate something like this after the foo x y pattern:

foo_lemma x y value = ?foo_lemma_rhs