: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
Change type class top level method generation

Don't put explicit arguments in the top level methods (i.e. make them
point free). This means that they will be more inclined to reduce, which
helps in particular with totality checking, but possibly also with
theorem proving.