2000-11-28 wenzelm 2000-11-28 tuned;
2000-11-28 wenzelm 2000-11-28 added consumes, consumes_default; added save; tuned;
2000-11-28 wenzelm 2000-11-28 resolveq_cases_tac: insert facts;
2000-11-28 wenzelm 2000-11-28 added "consumes" attribute;
2000-11-28 wenzelm 2000-11-28 consume facts;
2000-11-28 wenzelm 2000-11-28 consumes0/1;
2000-11-28 wenzelm 2000-11-28 RuleCases.save;
2000-11-27 nipkow 2000-11-27 *** empty log message ***
2000-11-27 paulson 2000-11-27 deleted unused result intrel_refl
2000-11-27 nipkow 2000-11-27 *** empty log message ***
2000-11-26 nipkow 2000-11-26 *** empty log message ***
2000-11-26 nipkow 2000-11-26 *** empty log message ***
2000-11-24 nipkow 2000-11-24 hide many names from Datatype_Universe.
2000-11-24 wenzelm 2000-11-24 exception Interrupt = SML90.Interrupt;
2000-11-24 paulson 2000-11-24 added exception Interrupt for use in function Library/try
2000-11-23 wenzelm 2000-11-23 arith_tac: atomize;
2000-11-23 wenzelm 2000-11-23 standard: close_derivation;
2000-11-23 wenzelm 2000-11-23 * HOL: syntax or "abs";
2000-11-23 nipkow 2000-11-23 *** empty log message ***
2000-11-22 wenzelm 2000-11-22 tuned;
2000-11-22 wenzelm 2000-11-22 tuned;
2000-11-22 wenzelm 2000-11-22 *** empty log message ***
2000-11-22 nipkow 2000-11-22 *** empty log message ***
2000-11-21 wenzelm 2000-11-21 tag result with name reference to final binding (basically just a comment);
2000-11-21 wenzelm 2000-11-21 Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-21 wenzelm 2000-11-21 replace \<dots>;
2000-11-21 wenzelm 2000-11-21 unsymbolize;
2000-11-21 wenzelm 2000-11-21 quote executable;
2000-11-21 wenzelm 2000-11-21 tuned;
2000-11-21 bauerg 2000-11-21 ;
2000-11-21 kleing 2000-11-21 adjusted for BV changes (Ok -> OK)
2000-11-21 paulson 2000-11-21 thebibliography environment: replaced the Springer version by the standard one in book.cls
2000-11-21 bauerg 2000-11-21 alternative function definition;
2000-11-21 nipkow 2000-11-21 *** empty log message ***
2000-11-20 kleing 2000-11-20 BCV integration (type system is semilattice)
2000-11-20 kleing 2000-11-20 BCV integration (first step)
2000-11-18 wenzelm 2000-11-18 export freeze_thaw_type;
2000-11-18 wenzelm 2000-11-18 improved messages;
2000-11-18 wenzelm 2000-11-18 default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18 wenzelm 2000-11-18 axclass ordered_ring; instance int :: ordered_ring;
2000-11-18 wenzelm 2000-11-18 quot_cond_function: simplified, support conditional definition;
2000-11-18 wenzelm 2000-11-18 abs_eq_0: #0 instead of 0;
2000-11-18 wenzelm 2000-11-18 symbol syntax for "abs";
2000-11-18 wenzelm 2000-11-18 added axclass ordered_field;
2000-11-17 wenzelm 2000-11-17 check result: Envir.beta_norm;
2000-11-17 wenzelm 2000-11-17 Envir.beta_norm;
2000-11-17 wenzelm 2000-11-17 added beta_norm; tuned;
2000-11-17 wenzelm 2000-11-17 tuned;
2000-11-17 wenzelm 2000-11-17 removed quot_cond_function1, quot_function1; removed overloaded standard operations;
2000-11-17 wenzelm 2000-11-17 UNIV_witness;
2000-11-17 wenzelm 2000-11-17 Ring_and_Field;
2000-11-17 wenzelm 2000-11-17 Library/Ring_and_Field.thy;
2000-11-16 bauerg 2000-11-16 rings and fields;
2000-11-16 wenzelm 2000-11-16 Proof.assert_forward;
2000-11-16 wenzelm 2000-11-16 added not_equiv_sym, not_equiv_trans1/2; tuned;
2000-11-16 wenzelm 2000-11-16 added abs_mult, abs_eq_0, square_nonzero;
2000-11-16 paulson 2000-11-16 ground terms section: new intro
2000-11-16 paulson 2000-11-16 CTT
2000-11-15 wenzelm 2000-11-15 separate rules for function/operation definitions;
2000-11-15 wenzelm 2000-11-15 renamed integ_le_less to int_le_less;