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

addss -> force_tac

named the primrec clauses of upt

renamed upt_Suc, since that name is needed for its primrec rule

new setsum results

tuned case_tac;

updated acknowledgements

fixed the documentation of goalw_cterm and prove_goalw_cterm

res_inst_tac, etc., no longer print the "dest_state" message when the selected subgoal does not exist

setsum replaces sum_below

moved mostly to HOL/SetInterval.ML and UNITY/UNITY.ML

sum_below moved here from Arith

improved error msgs, listing variable names

better indentation; declared function "null"

new default rules

deleted sum_below: no need for it with setsum and lessThan

documented permute_prems

better indentation

overloading of 0

added "done" proof;

proper token_translation for latex mode;

some lemmas about plus_ac0

setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.

setsum is now overloaded on plus_ac0

installing plus_ac0 for nat