| 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
|
| Thu, 25 Mar 2004 10:32:21 +0100 |
paulson |
new material from Avigad
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 10:34:49 +0100 |
paulson |
strengthened the axclass claims
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
| Fri, 19 Dec 2003 04:28:45 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Thu, 20 Feb 2003 11:10:24 +0100 |
paulson |
new inverse image lemmas
|
file |
diff |
annotate
|
| Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
file |
diff |
annotate
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
file |
diff |
annotate
|
| Fri, 27 Sep 2002 16:44:50 +0200 |
paulson |
Proof tidying
|
file |
diff |
annotate
|
| Fri, 20 Sep 2002 11:48:35 +0200 |
paulson |
less use of x-symbols
|
file |
diff |
annotate
|
| Mon, 12 Aug 2002 17:48:15 +0200 |
nipkow |
Added Mi and Max on sets, hid Min and Pls on numerals.
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 22:15:55 +0200 |
wenzelm |
simplified locale predicates;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2002 18:44:36 +0200 |
wenzelm |
accomodate cumulative locale predicates;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2002 12:08:45 +0200 |
wenzelm |
ACe_axioms;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 18:26:09 +0200 |
wenzelm |
adapted to locale defs;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 14:44:58 +0100 |
wenzelm |
lemmas (in ACe) AC;
|
file |
diff |
annotate
|
| Thu, 10 Jan 2002 01:10:58 +0100 |
wenzelm |
qualified exports from locales;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:38:55 +0100 |
wenzelm |
renamed theory Finite to Finite_Set and converted;
|
file |
diff |
annotate
|