| Tue, 26 Sep 2006 13:34:16 +0200 | haftmann | renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes | file | diff | annotate |
| Fri, 14 Jul 2006 14:37:15 +0200 | ballarin | Term.term_lpo takes order on terms rather than strings as argument. | file | diff | annotate |
| Mon, 27 Mar 2006 18:10:02 +0200 | paulson | removed illegal character codes | file | diff | annotate |
| Fri, 10 Mar 2006 15:33:48 +0100 | haftmann | renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc. | file | diff | annotate |
| Sat, 04 Feb 2006 03:14:32 +0100 | huffman | speedup: use simproc for AC rules | file | diff | annotate |
| Sat, 25 Jun 2005 16:06:17 +0200 | nipkow | Changes due to new abel_cancel.ML | file | diff | annotate |
| Fri, 17 Jun 2005 18:33:03 +0200 | wenzelm | renamed sg_ref to thy_ref; | file | diff | annotate |
| Tue, 18 May 2004 10:02:50 +0200 | obua | simplification for abelian groups | file | diff | annotate |