test_classrel/arity improve error reporting; tuned;

xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;

string_of_vname moved to term.ML;

incorporate sort ops from term.ML; use Graph.T; misc cleanup;

type.ML now before Syntax module;

xxx_typ_raw replace xxx_typ_no_norm forms;

'classrel' now allows multiple arguments;

Sign.certify_tyname;

TypeInfer.paramify_dummies, TypeInfer.param;

Args.local_typ_raw;

output_tym: removed duplicate clauses;

Graph.minimals;

adapted syntax to cope with lack of non-logical types;

Type.typ_instance;

load ML files only once;

removed duplicate thms;

Sign.typ_instance;

tuned message;

tuned document;

use plain SOME;

proper use of 'syntax';

auto update

has_consts now handles the @-operator

new bij_betw operator

more results about isomorphisms

conversion of Hilbert_Choice to Isar script

the function list1 has been exported.

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.