switched to Isar proofs

Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to the current context is now done automatically);

Toplevel.no_timing;

transfer now automatic;

removed 'transfer' att (is now automatic);

get_thm(s): automatic transfer;

tuned tactic emulation;

removed 'transfer' att;

moved some theorems to Finite.ML

added new proofs and simplified an old one

new theorems (some from Multiset)

the is now defined using primrec, avoiding explicit use of arbitrary.

cleaned up;

global timing flag;

fixed comment;

renamed trace/stat_norm_ast to trace/stat_ast;

renamed Syntax.trace_norm_ast to Syntax.trace_ast; removed Syntax.stat_norm_ast;

proof_timing replaced by global timing;

* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global timing flag supersedes proof_timing and Toplevel.trace;

Collect_neg_eq;

\newcommand{\indexisarcase};

case 'antecedent';

write major keywords;

sublist and some lemmas about it

a more robust proof

fixed the dependences

tidied

restored some of the lessThans