| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:22:22 +0100 |
haftmann |
dropped accidental duplication of "lin" prefix from cs. 108662d50512
|
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
|
| Mon, 11 May 2009 15:57:29 +0200 |
haftmann |
qualified names for Lin_Arith tactics and simprocs
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| Mon, 27 Apr 2009 10:11:44 +0200 |
haftmann |
cleaned up theory power further
|
file |
diff |
annotate
|
| Thu, 23 Apr 2009 12:17:51 +0200 |
haftmann |
adaptions due to rearrangment of power operation
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 16:56:20 +0200 |
huffman |
instance real_field < field_char_0;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 17:47:22 +0200 |
huffman |
move nonstandard analysis theories to NSA directory
|
file |
diff |
annotate
|