Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
moved constants inverse and divide to Ring.thy
|
file |
diff |
annotate
|
Mon, 08 Feb 2010 17:12:22 +0100 |
haftmann |
using code antiquotation
|
file |
diff |
annotate
|
Mon, 08 Feb 2010 14:06:43 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 17:21:48 +0100 |
hoelzl |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 00:24:38 +0100 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 20:41:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 08:57:35 +0100 |
chaieb |
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
|
file |
diff |
annotate
|