| Sun, 06 May 2007 21:49:23 +0200 | haftmann | tuned | file | diff | annotate |
| Sun, 21 Jan 2007 16:43:46 +0100 | wenzelm | simplified ML setup; | file | diff | annotate |
| Sat, 20 Jan 2007 14:09:11 +0100 | wenzelm | added @{clasimpset}; | file | diff | annotate |
| Wed, 06 Dec 2006 01:12:56 +0100 | wenzelm | simplified ML bindings -- moved to HOL.thy; | file | diff | annotate |
| Mon, 27 Nov 2006 13:42:47 +0100 | haftmann | introduced Simpdata structure | file | diff | annotate |
| Sun, 12 Nov 2006 21:14:49 +0100 | wenzelm | mk_atomize: careful matching against rules admits overloading; | file | diff | annotate |
| Fri, 03 Nov 2006 15:28:13 +0100 | haftmann | re-added simpdata.ML | file | diff | annotate |
| Mon, 16 Oct 2006 14:07:21 +0200 | haftmann | slight cleanup | file | diff | annotate |
| Wed, 11 Oct 2006 14:51:24 +0200 | haftmann | cleaned up HOL bootstrap | file | diff | annotate |
| Tue, 10 Oct 2006 10:35:24 +0200 | haftmann | cleanup basic HOL bootstrap | file | diff | annotate |
| Tue, 10 Oct 2006 09:17:18 +0200 | haftmann | fixed typo | file | diff | annotate |
| Sat, 07 Oct 2006 01:30:58 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 26 Jul 2006 19:23:04 +0200 | webertj | linear arithmetic splits certain operators (e.g. min, max, abs) | file | diff | annotate |
| Tue, 11 Jul 2006 12:16:52 +0200 | wenzelm | let_simproc: activate Variable.import; | file | diff | annotate |
| Sat, 08 Jul 2006 12:54:33 +0200 | wenzelm | Goal.prove_global; | file | diff | annotate |
| Wed, 05 Jul 2006 11:32:38 +0200 | schirmer | fixed let-simproc | file | diff | annotate |
| Wed, 26 Apr 2006 20:34:11 +0200 | wenzelm | removed obsolete expand_case_tac; | file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 | wenzelm | setup: theory -> theory; | file | diff | annotate |
| Sat, 31 Dec 2005 21:49:36 +0100 | wenzelm | removed obsolete Provers/make_elim.ML; | file | diff | annotate |
| Wed, 14 Dec 2005 18:01:50 +0100 | paulson | deleted redundant (looping!) simprule | file | diff | annotate |
| Thu, 01 Dec 2005 22:03:01 +0100 | wenzelm | unfold_tac: static evaluation of simpset; | file | diff | annotate |
| Wed, 16 Nov 2005 17:45:22 +0100 | wenzelm | Term.betapply; | file | diff | annotate |
| Tue, 25 Oct 2005 18:18:49 +0200 | wenzelm | avoid legacy goals; | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:38 +0200 | wenzelm | OldGoals; | file | diff | annotate |
| Tue, 18 Oct 2005 17:59:25 +0200 | wenzelm | Simplifier.theory_context; | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:10 +0200 | wenzelm | change_claset/simpset; | file | diff | annotate |
| Fri, 07 Oct 2005 20:41:10 +0200 | nipkow | changes due to new neq_simproc in simpdata.ML | file | diff | annotate |
| Mon, 12 Sep 2005 18:20:32 +0200 | haftmann | introduced new-style AList operations | file | diff | annotate |
| Wed, 31 Aug 2005 15:46:34 +0200 | wenzelm | simp_implies: proper named infix; | file | diff | annotate |
| Tue, 02 Aug 2005 19:47:13 +0200 | wenzelm | added unfold_tac (Simplifier.inherit_bounds); | file | diff | annotate |