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.