improved print of constructors in OCaml

changed syntax for axclass attach

removed obsolete cond_add_path;

removed obsolete context_thy etc.;

removed obsolete init_pgip; removed obsolete redo, context_thy etc.;

removed obsolete init_context;

obsolete (cf. ProofGeneral/proof_general_emacs.ML);

tuned;

signed_string_of_int;

added proper header;

added signed_string_of_int (pruduces proper - instead of SML's ~);

removed obsolete proof_general.ML;

minor tuning;

tuned specifications/proofs;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;

renamed Graph.project to Graph.subgraph;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;

renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;

Sorts.minimal_classes;

classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;

replaced classes by all_classes (topologically sorted); added minimal_classes;

replaced Sign.classes by Sign.all_classes (topologically sorted);

Enable new Proof General code again after SML/NJ compatibility fixes by Florian.

Typo in last commit

explicit construction of operational classes

added handling for explicit classrel witnesses

``classes`` now returns classes in topological order

dropped some bookkeeping

simplified class_package

use_ml: reverted to simple output (Poly/ML changed);