| Thu, 05 Jul 2007 00:06:10 +0200 | wenzelm | common normalizer_funs, avoid cterm_of; | file | diff | annotate |
| Sat, 23 Jun 2007 19:33:22 +0200 | nipkow | tuned and renamed group_eq_simps and ring_eq_simps | file | diff | annotate |
| Thu, 21 Jun 2007 15:42:12 +0200 | wenzelm | tuned comments; | file | diff | annotate |
| Thu, 14 Jun 2007 18:33:31 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Tue, 12 Jun 2007 10:15:32 +0200 | chaieb | algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts | file | diff | annotate |
| Mon, 11 Jun 2007 18:28:16 +0200 | chaieb | Conversion for computation on constants now depends on the context | file | diff | annotate |
| Mon, 11 Jun 2007 16:23:17 +0200 | chaieb | Added instantiation of algebra method to fields | file | diff | annotate |