| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Tue, 06 Jan 2004 10:40:15 +0100 |
paulson |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2003 10:41:39 +0100 |
paulson |
including 0 ~= 1 in definition of Field
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 22:57:52 +0200 |
wenzelm |
use generic 1 instead of Numeral1;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| Fri, 15 Dec 2000 17:59:45 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2000 16:22:10 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 22:08:49 +0100 |
wenzelm |
left_minus axiom;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 20:05:58 +0100 |
wenzelm |
added Library/Rational_Numbers.thy;
|
file |
diff |
annotate
|