Corrected printer bug for bounded quantifiers Q x<=y. P

more group isomorphisms

added drop_take:thm

- deleted unneeded function eta_long (now in Pure/pattern.ML - added HOL.min / HOL.max to allowed consts again - added final simplification step with presburger_ss to preprocessor again

Adapted to new syntax for case expressions.

Added more flexible parse / print translations for case expressions.

Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.

- exported result datatype - added functions get_result and get_exn

updated;

Pure: clear separation of logical types and nonterminals;

adapted tsig/sg interface;

added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;

added fold, product; removed transitive_closure;

adapted names of some sort ops;

major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;

Type.strip_sorts;

incorporate type inference interface from type.ML;

adapted tsig interface;

moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);

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;