polished the induction

put the flat at the right place (to avoid exceptions)

fixed variable exporting problem

compile

added induct tactic

tuning

renamed "mk_UnN" to "mk_UnIN"

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;

clarified markup names;

more general Document_Model.point_range; more general Document_View.Active_Area; eliminated dead popup material;

more static handling of rendering options;

tuned options (again);

more scalable option-group;

tuned

merged

tuned proofs;

remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced

workaround for HOL-Mirabelle-ex oddities;

instructions for quick start in 20min;

more liberal init_components: base dir may get created later when resolving missing components;

more efficient painting based on cached result;

more standard init_components -- particularly important to pick up correct jdk/scala version;

tuned

merged