| Sat, 20 Jan 2007 14:09:10 +0100 | wenzelm | added @{claset}; | file | diff | annotate |
| Sun, 26 Nov 2006 23:43:53 +0100 | wenzelm | converted legacy ML scripts; | 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 |
| Fri, 30 Dec 2005 16:56:56 +0100 | wenzelm | provide cla_dist_concl; | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:13 +0200 | wenzelm | change_claset/simpset; | file | diff | annotate |
| Wed, 20 Aug 2003 11:04:17 +0200 | paulson | new case_tac method | file | diff | annotate |
| Wed, 06 Mar 2002 17:56:02 +0100 | wenzelm | tuned; | file | diff | annotate |
| Sun, 14 Oct 2001 19:59:55 +0200 | wenzelm | eliminated atomize rules; | file | diff | annotate |
| Tue, 16 Jan 2001 00:28:50 +0100 | wenzelm | tuned atomize; | file | diff | annotate |
| Fri, 10 Nov 2000 19:00:22 +0100 | wenzelm | val atomize = thms "atomize'"; | file | diff | annotate |
| Fri, 03 Nov 2000 21:31:11 +0100 | wenzelm | "atomize" for classical tactics; | file | diff | annotate |
| Tue, 05 Sep 2000 18:43:22 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sun, 30 Jul 2000 13:01:50 +0200 | wenzelm | updated ObtainFun; | file | diff | annotate |
| Wed, 28 Jun 2000 10:37:52 +0200 | paulson | declaring and using cla_make_elim | file | diff | annotate |
| Wed, 05 Jan 2000 11:50:55 +0100 | wenzelm | ObtainFun; | file | diff | annotate |
| Wed, 25 Aug 1999 20:45:19 +0200 | wenzelm | proper bootstrap of IFOL/FOL theories and packages; | file | diff | annotate |
| Mon, 02 Aug 1999 18:10:26 +0200 | wenzelm | fixed Blast_Data; | file | diff | annotate |
| Wed, 18 Nov 1998 11:03:49 +0100 | wenzelm | blast: cla_method'; | file | diff | annotate |
| Wed, 25 Feb 1998 20:29:58 +0100 | oheimb | renamed rep_claset to rep_cs | file | diff | annotate |
| Tue, 23 Dec 1997 11:39:03 +0100 | paulson | Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac | file | diff | annotate |
| Wed, 26 Nov 1997 17:31:02 +0100 | paulson | The change from iffE to iffCE means fewer case splits in most cases. Very few | file | diff | annotate |
| Mon, 03 Nov 1997 12:28:14 +0100 | wenzelm | adapted to new implicit claset; | file | diff | annotate |
| Fri, 10 Oct 1997 15:52:12 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Wed, 06 Aug 1997 00:41:40 +0200 | berghofe | Moved functions from file "thy_data.ML". | file | diff | annotate |
| Wed, 02 Apr 1997 15:19:40 +0200 | paulson | Now builds blast_tac | file | diff | annotate |
| Thu, 27 Mar 1997 10:07:11 +0100 | paulson | Now uses the alternative (safe!) rules for ex1 | file | diff | annotate |
| Fri, 03 Jan 1997 15:01:55 +0100 | paulson | Implicit simpsets and clasets for FOL and ZF | file | diff | annotate |