2007-07-03 wenzelm 2007-07-03 removed obsolete mk_conjunction_list, intr/elim_list;
2007-07-03 wenzelm 2007-07-03 removed obsolete goals_conv (cf. prems_conv); added efficient goal_conv_rule; tuned comments;
2007-07-03 wenzelm 2007-07-03 Conjunction.intr/elim_balanced; CONVERSION tactical; tuned;
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical; Simplifier.rewrite_goal_tac;
2007-07-03 wenzelm 2007-07-03 Conjunction.mk_conjunction_balanced;
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical;
2007-07-03 nipkow 2007-07-03 Fixed problem with patterns in lambdas
2007-07-03 krauss 2007-07-03 fixed an issue with mutual recursion
2007-07-03 huffman 2007-07-03 instance pordered_comm_ring < pordered_ring
2007-07-02 nipkow 2007-07-02 Added pattern maatching for lambda abstraction
2007-07-02 paulson 2007-07-02 revised the discussion of type classes
2007-07-02 chaieb 2007-07-02 Generic QE need no Context anymore
2007-07-02 chaieb 2007-07-02 Handle exception TYPE
2007-07-02 chaieb 2007-07-02 Tuned proofs
2007-06-30 obua 2007-06-30 added ordered_ring and ordered_semiring
2007-06-29 haftmann 2007-06-29 tuned arithmetic modules
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-29 haftmann 2007-06-29 dropped local cg cmd
2007-06-28 haftmann 2007-06-28 dropped toplevel lcm, gcd
2007-06-28 haftmann 2007-06-28 proper collapse_let
2007-06-28 haftmann 2007-06-28 new code generator framework
2007-06-28 haftmann 2007-06-28 dropped Library.lcm
2007-06-28 haftmann 2007-06-28 tuned
2007-06-28 haftmann 2007-06-28 code generation for dvd
2007-06-28 haftmann 2007-06-28 simplified keyword setup
2007-06-27 paulson 2007-06-27 GPL -> BSD
2007-06-27 nipkow 2007-06-27 *** empty log message ***
2007-06-26 paulson 2007-06-26 updated for metis method
2007-06-26 paulson 2007-06-26 recoded
2007-06-26 paulson 2007-06-26 simplified
2007-06-26 paulson 2007-06-26 completed some references
2007-06-26 paulson 2007-06-26 changes for type class ring_no_zero_divisors
2007-06-26 nipkow 2007-06-26 *** empty log message ***
2007-06-26 nipkow 2007-06-26 added NBE
2007-06-26 nipkow 2007-06-26 removed removed lemmas
2007-06-26 wenzelm 2007-06-26 fixed undo: try undos_proof first!
2007-06-25 wenzelm 2007-06-25 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW; eta_long_tac; tuned;
2007-06-25 nipkow 2007-06-25 removed theorem
2007-06-25 nipkow 2007-06-25 removed redundant lemma
2007-06-25 nipkow 2007-06-25 removed redundant lemmas
2007-06-25 obua 2007-06-25 commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
2007-06-25 krauss 2007-06-25 removed "sum_tools.ML" in favour of BalancedTree
2007-06-25 wenzelm 2007-06-25 added eta_long_conversion;
2007-06-25 wenzelm 2007-06-25 added eta_long_tac;
2007-06-25 wenzelm 2007-06-25 added reasonably efficient add_cterm_frees;
2007-06-25 wenzelm 2007-06-25 made type conv pervasive; removed obsolete eta_conv (cf. Thm.eta_long_conv);
2007-06-25 wenzelm 2007-06-25 made type conv pervasive; Thm.eta_long_conversion; Thm.add_cterm_frees; tuned;
2007-06-25 wenzelm 2007-06-25 Thm.eta_long_conversion;
2007-06-25 wenzelm 2007-06-25 made type conv pervasive; Thm.add_cterm_frees;
2007-06-25 wenzelm 2007-06-25 Thm.add_cterm_frees;
2007-06-25 wenzelm 2007-06-25 made type conv pervasive;
2007-06-25 wenzelm 2007-06-25 made type conv pervasive; tuned;
2007-06-24 nipkow 2007-06-24 tex problem fixed
2007-06-24 nipkow 2007-06-24 tuned and used field_simps
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 new lemmas
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-22 huffman 2007-06-22 fix looping simp rule