Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
Sat, 06 Mar 2010 18:24:30 -0800 |
huffman |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
tuned text
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
Wed, 10 Feb 2010 15:52:12 +0100 |
haftmann |
dropped last occurence of the linlinordered accident
|
file |
diff |
annotate
|
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 |
division ring assumes divide_inverse
|
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
| base
|