Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Mon, 09 Aug 2004 10:09:44 +0200 |
nipkow |
Aded a thm.
|
file |
diff |
annotate
|
Wed, 04 Aug 2004 19:11:02 +0200 |
nipkow |
added some inj_on thms
|
file |
diff |
annotate
|
Thu, 22 Jul 2004 17:37:31 +0200 |
nipkow |
Modified \<Sum> syntax a little.
|
file |
diff |
annotate
|
Thu, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
Wed, 14 Jul 2004 10:25:03 +0200 |
nipkow |
added {0::nat..n(} = {..n(}
|
file |
diff |
annotate
|
Thu, 24 Jun 2004 17:52:55 +0200 |
paulson |
ringpower to recpower
|
file |
diff |
annotate
|
Tue, 15 Jun 2004 10:40:05 +0200 |
paulson |
strengthened some theorems
|
file |
diff |
annotate
|
Wed, 09 Jun 2004 11:18:51 +0200 |
paulson |
moved some cardinality results into main HOL
|
file |
diff |
annotate
|
Fri, 14 May 2004 16:52:53 +0200 |
paulson |
removed a premise of card_inj_on_le
|
file |
diff |
annotate
|
Wed, 12 May 2004 10:00:56 +0200 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
Fri, 23 Apr 2004 20:48:28 +0200 |
wenzelm |
tuned notation;
|
file |
diff |
annotate
|
Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
Thu, 01 Apr 2004 10:54:32 +0200 |
paulson |
new type class abelian_group
|
file |
diff |
annotate
|