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;

added clear_mss;

variant version;

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

close_block: transfer_used_names; tuned;

added transfer_used_names;

oops;

proper text;

tuned;

tuned print_state;

fixed 'txt';

pretty_thm: include oracles (!) in hyps;

skip_proof feature 'sorry' (for quick_and_dirty mode only);

generalized fixes get index 0;

added 'txt';

add_txt;

tuned;

fixed order_trans;

added KnasterTarski.thy;

renamed with/APP to of/OF;

Isar_examples/KnasterTarski.thy;

added with_facts(_i); also, finally: opt_rules;

'with' as == 'from' as facts; also, finally: opt_rules;

also, finally: opt_rules;

have_thmss: more_ths; simple_have_thmss;

have_thmss: more_ths;

renamed with/APP to of/OF;

tuned;

fixed backtracking of global_qed;

added check_result; setmp Display.show_hyps false; fixed auto_bind_facts; tuned finish_proof; fixed backtracking of global_qed;

setmp Display.show_hyps false;

fix, assume, presume: prf_asm;

added prf_asm;

expandshort

many new theorems concerning multiplication and (in)equations

now div and mod are overloaded; dvd is polymorphic

new laws mult_le_cancel1, mult_le_cancel2

antisym first;

more robust trans rules;

Isar.sync_main;

added sync;

sync token;

sync;

added sync marker;

New thm trancl_trans_induct

Bad translation fixed.

updated;

improved RANGE;

tuned;

cond_extern_table;

added presume command;

cond_extern_table; datatype method = Method of thm list -> tactic;

tuned print_state; datatype method = Method of thm list -> tactic; assumptions: back-pressure solver as parameter;

tuned output: print_context replaced by strings_of_context; assumptions: back-pressure solver as parameter;

cond_extern_table;

added cond_extern_table;

branching_level = 400;

tidied

renamed PPI to plam simplified the definition of lift_act

renamed PPI to plam

another non-working snapshot

new distributive laws involving * and -

rewrite rules to distribute CONSTANT multiplication over sum and difference; removed automatic rewriting of 2x to x+x

another snapshot, still not working