merged two commands

allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)

distinguish between nested and nesting BNFs

make tactic more robust in the case where "asm_simp_tac" already finishes the job

derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive

no longer react on global_settings (cf. 34ac36642a31);

refined output panel: more value-oriented approach to update and caret focus;