More Isar

Added Isar command also for tactic using Metis, and tinkered around
with stuff. Demo examples now neater.