Implement logging kernel on top of stdknl terms

The code from logging-kernel/Thm.{sig,sml} lives on but the other
stuff (duplicates of code from experimental-kernel) can be deleted.