| Sat, 28 Jan 2006 17:28:50 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 06 Jan 2006 18:18:13 +0100 | wenzelm | simplified EqSubst setup; | file | diff | annotate |
| Fri, 06 Jan 2006 15:18:20 +0100 | wenzelm | tuned EqSubst setup; | file | diff | annotate |
| Sat, 31 Dec 2005 21:49:39 +0100 | wenzelm | removed obsolete cla_dist_concl; | file | diff | annotate |
| Fri, 30 Dec 2005 16:56:56 +0100 | wenzelm | provide cla_dist_concl; | file | diff | annotate |
| Fri, 23 Dec 2005 18:36:26 +0100 | wenzelm | removed obsolete induct_atomize_old; | file | diff | annotate |
| Thu, 22 Dec 2005 00:28:34 +0100 | wenzelm | updated auxiliary facts for induct method; | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Tue, 01 Feb 2005 18:01:57 +0100 | paulson | the new subst tactic, by Lucas Dixon | file | diff | annotate |
| Thu, 08 Jul 2004 19:32:46 +0200 | wenzelm | removed obsolete dependency; | file | diff | annotate |
| Wed, 20 Aug 2003 11:04:17 +0200 | paulson | new case_tac method | file | diff | annotate |
| Tue, 01 Jul 2003 10:50:26 +0200 | paulson | moved some lemmas here from ZF | file | diff | annotate |
| Fri, 30 Aug 2002 16:42:45 +0200 | paulson | removal of blast.overloaded | file | diff | annotate |
| Wed, 05 Dec 2001 02:59:49 +0100 | wenzelm | removed declaration of disjI1, disjI2 (already done in IFOL); | file | diff | annotate |
| Wed, 28 Nov 2001 00:37:08 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 19 Nov 2001 20:46:05 +0100 | wenzelm | induct method: localize rews for rule; | file | diff | annotate |
| Mon, 12 Nov 2001 23:26:18 +0100 | wenzelm | induct_atomize: include atomize_conj (for mutual induction); | file | diff | annotate |
| Mon, 12 Nov 2001 20:22:23 +0100 | wenzelm | val local_imp_def = thm "induct_implies_def"; | file | diff | annotate |
| Fri, 09 Nov 2001 22:50:32 +0100 | wenzelm | theorems case_split = case_split_thm [case_names True False, cases type: o]; | file | diff | annotate |
| Wed, 31 Oct 2001 01:19:58 +0100 | wenzelm | induct_impliesI; | file | diff | annotate |
| Sat, 20 Oct 2001 20:18:45 +0200 | wenzelm | calculational rules moved from FOL to IFOL; | file | diff | annotate |
| Sun, 14 Oct 2001 22:15:07 +0200 | wenzelm | moved rulify to ObjectLogic; | file | diff | annotate |
| Thu, 04 Oct 2001 15:28:26 +0200 | wenzelm | moved atomize stuff to theory IFOL; | file | diff | annotate |
| Sun, 11 Feb 2001 16:31:54 +0100 | wenzelm | tuned trans rules; | file | diff | annotate |
| Fri, 10 Nov 2000 19:00:51 +0100 | wenzelm | added atomize_eq; | file | diff | annotate |
| Fri, 03 Nov 2000 21:31:11 +0100 | wenzelm | "atomize" for classical tactics; | file | diff | annotate |
| Mon, 02 Oct 2000 15:13:32 +0200 | wenzelm | added == transitive rule (bad idea??); | file | diff | annotate |
| Thu, 07 Sep 2000 20:47:34 +0200 | wenzelm | setup Rulify.setup; | file | diff | annotate |
| Tue, 29 Aug 2000 00:55:31 +0200 | wenzelm | cong setup now part of Simplifier; | file | diff | annotate |
| Fri, 04 Aug 2000 22:54:49 +0200 | wenzelm | lemmas atomize = all_eq imp_eq; | file | diff | annotate |
| Tue, 01 Aug 2000 11:58:14 +0200 | wenzelm | improved comments; | file | diff | annotate |
| Fri, 31 Mar 2000 22:22:23 +0200 | wenzelm | added cong atts; | file | diff | annotate |
| Wed, 15 Mar 2000 18:42:13 +0100 | wenzelm | splitter setup; | file | diff | annotate |
| Wed, 25 Aug 1999 20:45:19 +0200 | wenzelm | proper bootstrap of IFOL/FOL theories and packages; | file | diff | annotate |
| Mon, 16 Nov 1998 11:11:42 +0100 | wenzelm | attrib_setup; | file | diff | annotate |
| Wed, 29 Apr 1998 11:29:39 +0200 | wenzelm | tuned setup; | file | diff | annotate |
| Sat, 04 Apr 1998 12:28:39 +0200 | wenzelm | replaced thy_data by thy_setup; | file | diff | annotate |
| Mon, 03 Nov 1997 12:26:58 +0100 | wenzelm | added claset thy_data; | file | diff | annotate |
| Thu, 16 Sep 1993 12:20:38 +0200 | clasohm | Initial revision | file | diff | annotate |