export init_state; end_proof: reset goal_facts;

more renaming of theorems from _nat to _int (corresponding to a function that was similarly renamed some time ago Also new theorem zmult_int

more renaming of theorems from _nat to _int (corresponding to a function that was similarly renamed some time ago

qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int

qed_goal -> Goal

tuned;

tuned comments;

tuned contradiction method; improved comments;

improved comment;

more marg_comments;

Deriving rules in Isabelle;

rewrite add1_zle_eq is no longer in the default simpset

optimization for division by powers of 2

new montonicity theorems

new constant folding rewrites

handle cgoal;

added mk_cgoal, assume_goal;

same_tac;

change to force (m div 0 = 0)

many new theorems

renamed inj_nat to inj_int

new monotonicity theorems

new theorem zmult_eq_0_iff

renamed sort "numeral" to "number"

simplified the <= monotonicity proof

local qeds: print rule;

added show_hyps flag;

local qed; print rule;

term/prop: include number; method args: exlude method meta chars;

added show_hyps flag; local qed: print rule;

export assumption_tac; local qeds: print rule; same_tac: actually insert rules, !! bind vars;

removed merge_theories;

removed metacuts_tac;

tmp_path: *add* path;

thms_containing: undeclared consts error;

removed pretty_thm_no_hyps (again);

removed merge_theories;

may get BASH_PATH etc. from env;

new theorems for the "at most" relation

def: ==;

tuned Interrupt msgs;

pass exn;

handle THM exn;

handle THM/TERM exn;

dup_elim: use try to handle general exn;

handle THM exn;

fixed interrupts (eliminated races);

defer_tac: use try for general exn handling;

Symtab.lookup_multi;

more specific exn;

err_method: pass exn; nontriv_merge: no handle_error;

prove_goalw_cterm_general: pass exeption;

try/can: pass Interrupt and ERROR; nth_elem_string: use try;

rmdir pdf;

mono: extra I/E;

mono: AddXI/Es;

type claset: added extra I/E rules;

added Isar/local_defs.ML;

added 'def'; added "!!" keyword; removed 'qed_with';

added local_def(_i); removed global_qed_with(_i);

global_qed: removed alt_name, alt_att;

global_qed: removed alt_name, alt_att; setup_goal: proper order of prems;

added termp;

COMP: optional position;

write_keywords: default file name;

added compose_single;

added HOL.trans;

removed qed_with;

faster division algorithm; monotonicity of div in 2nd arg

more monotonicity laws for times

products of signs as equivalences

-B option;

removed old version; tuned;

tuned indentation;

added export_chain; propp: 'concl' patterns; terminal_proof: 2nd method; use Display.pretty_thm_no_hyps;

propp: 'concl' patterns; added 'thence';

propp: 'concl' patterns;

terminal_proof: 2nd method;

'export';

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;

removed nesting (unused);

export term_of_typ;

begin_theory: disallow finished;