changed header to cope with default if_weak_cong

Now if_weak_cong is a standard congruence rule

Introduction of integer division algorithm Renaming of theorems from _nat0 to _int0 and _nat1 to _int1

tidied proofs to cope with default if_weak_cong

Now if_weak_cong is a standard congruence rule

new theory IntDiv.thy

new files IntDiv.{thy,ML}

tuned output;

simp only: attribute, method arg; asm_simp method;

use generic numeral encoding and syntax;

adapted to generic numerals;

simp only;

added Numeral.thy;

_reflcl;

added Numeral.thy, Tools/numeral_syntax.ML;

removed proof history nesting commands (not useful);

improved errors;

removed nesting (unused);

export term_of_typ;

begin_theory: disallow finished;

added clear_mss;

variant version;

fixed scope of x:??H; improved final reasoning: fully formal now;

close_block: transfer_used_names; tuned;