| Tue, 08 Jun 2004 16:22:30 +0200 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| Tue, 19 Aug 2003 13:54:20 +0200 |
paulson |
new case_tac
|
file |
diff |
annotate
|
| Thu, 10 Jul 2003 17:14:41 +0200 |
paulson |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
|
file |
diff |
annotate
|
| Tue, 27 May 2003 11:39:03 +0200 |
paulson |
updating ZF-UNITY with Sidi's new material
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 13:26:10 +0200 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
file |
diff |
annotate
|
| Sun, 14 Jul 2002 19:59:55 +0200 |
paulson |
Removal of mono.thy
|
file |
diff |
annotate
|
| Sun, 14 Jul 2002 15:11:21 +0200 |
paulson |
merged Update with func
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 13:28:08 +0200 |
paulson |
Tidying and introduction of various new theorems
|
file |
diff |
annotate
|
| Wed, 26 Jun 2002 10:26:46 +0200 |
paulson |
new theorems
|
file |
diff |
annotate
|
| Wed, 19 Jun 2002 09:03:34 +0200 |
paulson |
conversion of Cardinal, CardinalArith
|
file |
diff |
annotate
|
| Tue, 18 Jun 2002 17:58:21 +0200 |
paulson |
new lemma
|
file |
diff |
annotate
|
| Fri, 24 May 2002 16:55:46 +0200 |
paulson |
strong lemmas about functions
|
file |
diff |
annotate
|
| Fri, 24 May 2002 13:15:37 +0200 |
paulson |
conversion of Perm to Isar. Strengthening of comp_fun_apply
|
file |
diff |
annotate
|
| Thu, 23 May 2002 17:05:21 +0200 |
paulson |
new definition of "apply" and new simprule "beta_if"
|
file |
diff |
annotate
|
| Wed, 22 May 2002 19:34:01 +0200 |
paulson |
more tidying
|
file |
diff |
annotate
|
| Wed, 22 May 2002 18:11:57 +0200 |
paulson |
tidying up
|
file |
diff |
annotate
|
| Tue, 21 May 2002 13:06:36 +0200 |
paulson |
converted domrange to Isar and merged with equalities
|
file |
diff |
annotate
|
| Sat, 18 May 2002 20:08:17 +0200 |
paulson |
converted Arith, Univ, func to Isar format!
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Mon, 15 Aug 1994 18:04:10 +0200 |
lcp |
ZF/func/empty_fun: renamed from fun_empty
|
file |
diff |
annotate
|
| Tue, 16 Nov 1993 14:24:21 +0100 |
clasohm |
made pseudo theories for all ML files;
|
file |
diff |
annotate
|