simplified prove_conv;

removed ':' from category of symbolic identifier chars;

query/bang_colon: separate tokens;

purged website sources

added strip_abs_eta

added chop_prefix

class_of_param instead of class_of

adaptions in class_package

adaptions in codegen

variants: special treatment of empty name;

avoid reference to internal skolem;

separate names filed (covers fixes/defaults);

adapted Name.defaults_of;

removed obsolete xless; tuned zero_var_indexes;

clean: no special treatment of empty name; declare, invent: clean arguments;

removed obsolete xless;

replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes

uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;

replaced read_radixint by read_intinf;

removed str_to_int in favour of general Syntax.read_xnum;

num/xnum: bin or hex;

Name.internal; Name.invent_list;

tuned;

* Pure: structure Name;

Names of basic logical entities (variables etc.).

replaced Term.variant(list) by Name.variant(_list); removed obsolete mem_term;

Name.internal; Name.dest_skolem;

adapted to more efficient Name/Variable implementation; removed dead code;

replaced Term.variant(list) by Name.variant(_list); Name.internal;

maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);