| 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
|