Adapted to new naming scheme for definitions.

Changed name of raw definition.

Name of ML function "not" is now qualified in order to avoid clashes with names of constants introduced by the user.

consts in consts_code Isar commands are now referred to by usual term syntax

size [nat] is identity

explicit import of Datatype.thy due to hook bootstrap problem

localized Sup/Inf

localized Min/Max

tuned

fix proofs

remove redundant lemmas

lemmas iszero_(h)complex_number_of are no longer needed

instance real_algebra_1 < ring_char_0

new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas

moved conversions to structure Conv; get_axiom_i;

added dest_fun/fun2/arg1; removed dest_binop; renamed cterm_(fo_)match to (fo_)match; renamed cterm_incr_indexes to incr_indexes_cterm;

tuned argument_type_of;

added destructors from drule.ML; added mk_binop;

moved some operations to more_thm.ML and conv.ML;

Conversions: primitive equality reasoning (from drule.ML);

added conv.ML;

Thm.match;

moved some Drule operations to Thm (see more_thm.ML);

Thm.first_order_match;

moved conversions to structure Conv;

"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"

add lemma norm_diff_ineq; shorten other proofs

removed Complex/ComplexBin.thy;

tuned ML setup;

tuned syntax;

eliminated unnamed infixes;

removed unused mk_cond_defpair;