| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
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
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:27 +0100 |
haftmann |
hide fact Nat.add_0_right; make add_0_right from Groups priority
|
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
|
| Thu, 29 Oct 2009 22:16:12 +0100 |
haftmann |
moved some lemmas to theory Int
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:18 +0200 |
haftmann |
tuned code postprocessor
|
file |
diff |
annotate
|
| Mon, 11 May 2009 19:51:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Mon, 11 May 2009 08:28:49 -0700 |
huffman |
newline at end of file
|
file |
diff |
annotate
|