simplify types of path operations (use real instead of real^1)

add lemmas convex_real_interval and convex_box

generalize more constants and lemmas

generalize constant closest_point

minimize imports

fix imports

document generation for Multivariate_Analysis

move l2-norm stuff into separate theory file

convert proofs to Isar-style

Library/Fraction_Field.thy: ordering relations for fractions

renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;

more systematic treatment of data -- avoid slightly odd nested tuples here; tuned;

replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;

misc tuning and simplification;

simplified some private bindings;

classrel and arity completion by krauss/schropp;

removed obsolete/unused Proof.match_bind;

modernized naming conventions of main Isar proof elements;

goals: simplified handling of implicit variables -- removed obsolete warning;

updated generated files;

cover 'schematic_lemma' etc.;

mark schematic statements explicitly;

eliminated spurious schematic statements;

explicit 'schematic_theorem' etc. for schematic theorem statements;

collapse category "schematic goal" in keyword table -- Proof General does not know about this;

added keyword category "schematic goal", which prevents any attempt to fork the proof;

merged

merged

separated instantiation of division_by_zero

epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance