| 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 |
| Thu, 08 Dec 2005 20:16:04 +0100 | wenzelm | swap: no longer pervasive; | file | diff | annotate |
| Thu, 08 Dec 2005 12:50:03 +0100 | wenzelm | Classical.swap; | file | diff | annotate |
| Tue, 06 Dec 2005 17:26:26 +0100 | haftmann | removed thms 'swap' and 'nth_map' from ML toplevel | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:13 +0200 | wenzelm | change_claset/simpset; | file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 | skalberg | Move towards standard functions. | file | diff | annotate |
| Tue, 04 Dec 2001 02:01:31 +0100 | wenzelm | hyp_subst_tac'; | file | diff | annotate |
| Sun, 14 Oct 2001 20:02:59 +0200 | wenzelm | improved atomize setup; | file | diff | annotate |
| Wed, 25 Jul 2001 13:13:01 +0200 | paulson | partial restructuring to reduce dependence on Axiom of Choice | file | diff | annotate |
| Sun, 22 Jul 2001 21:31:00 +0200 | wenzelm | the_equality [intro]; | 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, 17 Oct 2000 10:21:12 +0200 | paulson | renaming of contrapos rules | file | diff | annotate |
| Thu, 12 Oct 2000 12:16:22 +0200 | paulson | renamed ?Pa to ?Q in swap | file | diff | annotate |
| Fri, 15 Sep 2000 12:39:57 +0200 | paulson | renamed (most of...) the select rules | file | diff | annotate |
| Tue, 05 Sep 2000 18:43:22 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 04 Aug 2000 22:57:37 +0200 | wenzelm | val rev_eq_reflection = def_imp_eq; | 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:49:02 +0200 | wenzelm | proper bootstrap of HOL theory and packages; | file | diff | annotate |
| Mon, 02 Aug 1999 17:58:46 +0200 | wenzelm | tuned; | file | diff | annotate |
| Thu, 15 Jul 1999 10:27:54 +0200 | paulson | qed_goal -> Goal | 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 |
| Thu, 08 Jan 1998 18:09:07 +0100 | oheimb | added select_equality to the implicit claset | 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 |