deleted leading space in the definition of fresh
Added (optional) arguments to the tactics
fixed case names in the weak induction principle and
1) have adjusted the swapping of the result type
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
simplified the abs_supp_approx proof and tuned some comments in
tuned my last commit
tunings of some comments (nothing serious)