propp: 'concl' patterns; assumptions: tactics for non-goal export; use Display.pretty_thm_no_hyps; assm vs. assume vs. presume; tuned type goal; tuned print_goal; relative exports, absolute export_thm rule; transfer_facts; tuned;

propp: 'concl' patterns; assumptions: tactics for non-goal export; use Display.pretty_thm_no_hyps;

improved error msgs of cterm_instantiate; fixed incr_indexes;

aprop: ??id, ...;

improved error msgs of instantiate;

added commute: 'a seq list -> 'a list seq;

added pretty_thm_no_hyps;

theorems involving oracles are now printed with a suffixed [!];

Theorems involving oracles will be printed with a suffixed \verb|[!]|;

updated usedir;

integer division

Renaming of theorems from _nat0 to _int0 and _nat1 to _int1

Introduction of integer division algorithm

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;