| Tue, 18 Sep 2007 18:52:17 +0200 |
ballarin |
Simplified proofs due to transitivity reasoner setup.
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:18 +0200 |
haftmann |
moved class dense_linear_order to Orderings.thy
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 12:21:17 +0200 |
chaieb |
Axioms for class no longer use object-universal quantifiers
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:28 +0200 |
haftmann |
turned locales intro classes
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:22:49 +0200 |
wenzelm |
fixed dummyT (used as constraint);
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 09:31:19 +0200 |
chaieb |
Tuned document
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 23:23:39 +0200 |
wenzelm |
fixed document;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 17:53:45 +0200 |
chaieb |
Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution.
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 23:28:44 +0200 |
huffman |
spelling
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:06 +0200 |
wenzelm |
Dense linear order witout endpoints
|
file |
diff |
annotate
|