added subversion treatment

classes: prefer thy operations; accomodate tuned interfaces of Logic/Sign/AxClass;

export pretty_classrel/arity;

'axclass': no parameters;

tuned;

removed superclasses (see sign.ML);

added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);

added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;

moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;

Moved stuff from Ring_and_Field to Matrix

Adapted to changed type of add_typedef_i.

Hoare(Parallel) dependencies on document/*

added references

Minimal doc

Included cyclic list examples

fixed value restriction

Added splicing algorithm.

hide (open) const;

simplified AxClass.add_axclass interface;

added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;

removed unused class_le_path, sort_less;

add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;

Term.itselfT;

Added function "splice"

Even/Odd: avoid clash with even/odd of Main HOL;

results: smart_pretty_thm uses adhoc proof context if possible;

added full_name; abbrevs: mode does not affect name space;

add_syntax: actually observe print mode;