| Wed, 14 Sep 2005 23:14:59 +0200 |
wenzelm |
imports Commutative_Ring instead of Main, since the latter hides our names;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:14:58 +0200 |
wenzelm |
hide the rather generic names used in theory Commutative_Ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:14:57 +0200 |
wenzelm |
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:06:02 +0200 |
schirmer |
... prem19
|
changeset |
files
|
| Wed, 14 Sep 2005 23:04:59 +0200 |
schirmer |
added prem10 - prem19
|
changeset |
files
|
| Wed, 14 Sep 2005 23:03:52 +0200 |
schirmer |
removed syntax fun_map_comp;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:00:03 +0200 |
chaieb |
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
|
changeset |
files
|
| Wed, 14 Sep 2005 22:18:55 +0200 |
wenzelm |
Method comm_ring for proving equalities in commutative rings.
|
changeset |
files
|
| Wed, 14 Sep 2005 22:08:08 +0200 |
wenzelm |
tuned headers etc.;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:38 +0200 |
wenzelm |
fixed some ML names;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:37 +0200 |
wenzelm |
imports Commutative_Ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:36 +0200 |
wenzelm |
HOL: method comm_ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:34 +0200 |
wenzelm |
no longer prefer xemacs, which fails more often than GNU emacs;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:33 +0200 |
wenzelm |
Bernhard Haeupler: comm_ring;
|
changeset |
files
|