1999-07-02 ago wenzelm skip_proof feature 'sorry' (for quick_and_dirty mode only);
1999-07-02 ago wenzelm generalized fixes get index 0;
1999-07-02 ago wenzelm added 'txt';
1999-07-02 ago wenzelm add_txt;
1999-07-02 ago wenzelm tuned;
1999-07-01 ago wenzelm fixed order_trans;
1999-07-01 ago wenzelm added KnasterTarski.thy;
1999-07-01 ago wenzelm renamed with/APP to of/OF;
1999-07-01 ago wenzelm Isar_examples/KnasterTarski.thy;
1999-07-01 ago wenzelm added with_facts(_i);
1999-07-01 ago wenzelm 'with' as == 'from' as facts;
1999-07-01 ago wenzelm also, finally: opt_rules;
1999-07-01 ago wenzelm have_thmss: more_ths;
1999-07-01 ago wenzelm have_thmss: more_ths;
1999-07-01 ago wenzelm renamed with/APP to of/OF;
1999-07-01 ago wenzelm tuned;
1999-07-01 ago wenzelm fixed backtracking of global_qed;
1999-07-01 ago wenzelm added check_result;
1999-07-01 ago wenzelm setmp Display.show_hyps false;
1999-07-01 ago wenzelm fix, assume, presume: prf_asm;
1999-07-01 ago wenzelm added prf_asm;
1999-07-01 ago paulson expandshort
1999-07-01 ago paulson many new theorems concerning multiplication and (in)equations
1999-07-01 ago paulson now div and mod are overloaded; dvd is polymorphic
1999-07-01 ago paulson new laws mult_le_cancel1, mult_le_cancel2
1999-06-30 ago wenzelm antisym first;
1999-06-30 ago wenzelm more robust trans rules;
1999-06-30 ago wenzelm Isar.sync_main;
1999-06-30 ago wenzelm added sync;
1999-06-30 ago wenzelm sync token;
1999-06-30 ago wenzelm sync;
1999-06-30 ago wenzelm added sync marker;
1999-06-30 ago nipkow New thm trancl_trans_induct
1999-06-29 ago nipkow Bad translation fixed.
1999-06-28 ago wenzelm updated;
1999-06-28 ago wenzelm improved RANGE;
1999-06-28 ago wenzelm tuned;
1999-06-28 ago wenzelm cond_extern_table;
1999-06-28 ago wenzelm added presume command;
1999-06-28 ago wenzelm cond_extern_table;
1999-06-28 ago wenzelm tuned print_state;
1999-06-28 ago wenzelm tuned output: print_context replaced by strings_of_context;
1999-06-28 ago wenzelm cond_extern_table;
1999-06-28 ago wenzelm added cond_extern_table;
1999-06-25 ago wenzelm branching_level = 400;
1999-06-23 ago paulson tidied
1999-06-23 ago paulson renamed PPI to plam
1999-06-23 ago paulson renamed PPI to plam
1999-06-23 ago paulson another non-working snapshot
1999-06-23 ago paulson new distributive laws involving * and -
1999-06-23 ago paulson rewrite rules to distribute CONSTANT multiplication over sum and difference;
1999-06-17 ago paulson another snapshot, still not working
1999-06-17 ago paulson new results about SKIP
1999-06-17 ago paulson addition of drop_... operators with new results and simplification of old ones
1999-06-17 ago paulson renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
1999-06-17 ago paulson many new guarantees laws
1999-06-17 ago paulson moved image_UNION to Fun/image_UN
1999-06-17 ago paulson expandshort
1999-06-17 ago paulson renamed UNION_... to UN_... (to fit the convention)
1999-06-17 ago paulson renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT