| Wed, 11 Jul 2007 11:46:44 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 13:48:00 +0200 |
paulson |
new simprules Int_subset_iff and Un_subset_iff
|
file |
diff |
annotate
|
| Fri, 15 Aug 2003 13:07:01 +0200 |
paulson |
A document for UNITY
|
file |
diff |
annotate
|
| Mon, 31 Mar 2003 12:29:54 +0200 |
paulson |
more comments and tweaks
|
file |
diff |
annotate
|
| Wed, 26 Mar 2003 12:25:56 +0100 |
paulson |
Proofs for section 4.5.3
|
file |
diff |
annotate
|
| Fri, 21 Mar 2003 18:16:18 +0100 |
paulson |
More on progress sets
|
file |
diff |
annotate
|
| Tue, 18 Mar 2003 18:07:06 +0100 |
paulson |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
|
file |
diff |
annotate
|
| Mon, 17 Mar 2003 17:37:48 +0100 |
paulson |
More "progress set" material
|
file |
diff |
annotate
|
| Fri, 14 Mar 2003 10:30:46 +0100 |
paulson |
Proved the main lemma on progress sets
|
file |
diff |
annotate
|
| Mon, 10 Mar 2003 16:21:06 +0100 |
paulson |
New theory ProgressSets. Definition of closure sets
|
file |
diff |
annotate
|