| Sat, 23 Jun 2007 19:33:22 +0200 | nipkow | tuned and renamed group_eq_simps and ring_eq_simps | file | diff | annotate |
| Wed, 20 Jun 2007 19:49:14 +0200 | huffman | avoid using implicit prems in assumption | file | diff | annotate |
| Wed, 20 Jun 2007 05:18:39 +0200 | huffman | change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems | file | diff | annotate |
| Sun, 17 Jun 2007 18:47:03 +0200 | nipkow | tuned laws for cancellation in divisions for fields. | file | diff | annotate |
| Sun, 17 Jun 2007 13:39:50 +0200 | chaieb | moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs | file | diff | annotate |
| Fri, 15 Jun 2007 15:10:32 +0200 | nipkow | made divide_self a simp rule | file | diff | annotate |
| Tue, 05 Jun 2007 16:31:10 +0200 | chaieb | lemma lemma_DERIV_subst moved to Deriv.thy | file | diff | annotate |