| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
| base
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
| base
|
| Tue, 22 Apr 2008 08:33:19 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 04 Feb 2008 17:00:01 +0100 |
chaieb |
replaced class by locale
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 23:21:06 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 22:03:21 +0200 |
haftmann |
added proper subclass concept; improved class target
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:24 +0200 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| 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
|