1999-07-08 wenzelm added commute: 'a seq list -> 'a list seq;
1999-07-08 wenzelm added pretty_thm_no_hyps;
1999-07-08 wenzelm theorems involving oracles are now printed with a suffixed [!];
1999-07-08 wenzelm Theorems involving oracles will be printed with a suffixed \verb|[!]|;
1999-07-08 wenzelm updated usedir;
1999-07-08 paulson integer division
1999-07-08 paulson Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
1999-07-08 paulson Introduction of integer division algorithm
1999-07-08 paulson changed header to cope with default if_weak_cong
1999-07-08 paulson Now if_weak_cong is a standard congruence rule
1999-07-08 paulson Introduction of integer division algorithm
1999-07-08 paulson tidied proofs to cope with default if_weak_cong
1999-07-08 paulson Now if_weak_cong is a standard congruence rule
1999-07-08 paulson new theory IntDiv.thy
1999-07-08 paulson new files IntDiv.{thy,ML}
1999-07-06 wenzelm tuned output;
1999-07-06 wenzelm simp only: attribute, method arg;
1999-07-06 wenzelm use generic numeral encoding and syntax;
1999-07-06 wenzelm adapted to generic numerals;
1999-07-06 wenzelm simp only;
1999-07-06 wenzelm added Numeral.thy;
1999-07-06 wenzelm _reflcl;
1999-07-06 wenzelm added Numeral.thy, Tools/numeral_syntax.ML;
1999-07-06 wenzelm removed proof history nesting commands (not useful);
1999-07-06 wenzelm improved errors;
1999-07-06 wenzelm removed nesting (unused);
1999-07-06 wenzelm export term_of_typ;
1999-07-06 wenzelm begin_theory: disallow finished;
1999-07-06 wenzelm added clear_mss;
1999-07-05 wenzelm variant version;
1999-07-04 wenzelm fixed scope of x:??H;
1999-07-04 wenzelm close_block: transfer_used_names;
1999-07-04 wenzelm added transfer_used_names;
1999-07-02 wenzelm oops;
1999-07-02 wenzelm proper text;
1999-07-02 wenzelm tuned;
1999-07-02 wenzelm tuned print_state;
1999-07-02 wenzelm fixed 'txt';
1999-07-02 wenzelm pretty_thm: include oracles (!) in hyps;
1999-07-02 wenzelm skip_proof feature 'sorry' (for quick_and_dirty mode only);
1999-07-02 wenzelm generalized fixes get index 0;
1999-07-02 wenzelm added 'txt';
1999-07-02 wenzelm add_txt;
1999-07-02 wenzelm tuned;
1999-07-01 wenzelm fixed order_trans;
1999-07-01 wenzelm added KnasterTarski.thy;
1999-07-01 wenzelm renamed with/APP to of/OF;
1999-07-01 wenzelm Isar_examples/KnasterTarski.thy;
1999-07-01 wenzelm added with_facts(_i);
1999-07-01 wenzelm 'with' as == 'from' as facts;
1999-07-01 wenzelm also, finally: opt_rules;
1999-07-01 wenzelm have_thmss: more_ths;
1999-07-01 wenzelm have_thmss: more_ths;
1999-07-01 wenzelm renamed with/APP to of/OF;
1999-07-01 wenzelm tuned;
1999-07-01 wenzelm fixed backtracking of global_qed;
1999-07-01 wenzelm added check_result;
1999-07-01 wenzelm setmp Display.show_hyps false;
1999-07-01 wenzelm fix, assume, presume: prf_asm;
1999-07-01 wenzelm added prf_asm;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip