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;
2000-11-15 wenzelm 2000-11-15 updated;
2000-11-15 wenzelm 2000-11-15 isabellebody: \par at begin/end;
2000-11-14 paulson 2000-11-14 auto update
2000-11-14 paulson 2000-11-14 first version of Advanced Inductive Defs section
2000-11-14 paulson 2000-11-14 x-symbol support for Pi, Sigma, -->, : (membership) note that "lam" is displayed as TWO lambda-symbols
2000-11-14 paulson 2000-11-14 new Main.thy as in HOL, ZF
2000-11-13 wenzelm 2000-11-13 added read_terms, read_props (simulataneous type-inference);
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-11-13 wenzelm 2000-11-13 tuned IsarThy.theorem_i;
2000-11-13 kleing 2000-11-13 added students
2000-11-13 nipkow 2000-11-13 Removed > and >=
2000-11-13 nipkow 2000-11-13 Removed > and >= again.
2000-11-12 wenzelm 2000-11-12 quot_cond_definition;
2000-11-12 wenzelm 2000-11-12 simplified induction;
2000-11-12 wenzelm 2000-11-12 updated;
2000-11-12 wenzelm 2000-11-12 "induct" method: handle proper rules;
2000-11-12 wenzelm 2000-11-12 removed warning for "stripped" option;
2000-11-12 wenzelm 2000-11-12 removed junk;
2000-11-12 wenzelm 2000-11-12 Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-11-10 wenzelm 2000-11-10 * added overloaded operations "inverse" and "divide" (infix "/");