| Thu, 30 Apr 2009 12:16:35 -0700 |
huffman |
used named theorems for declaring numeral simps
|
file |
diff |
annotate
|
| Thu, 30 Apr 2009 11:14:04 -0700 |
huffman |
clean up unsigned numeral proofs
|
file |
diff |
annotate
|
| Thu, 30 Apr 2009 07:33:40 -0700 |
huffman |
detect error cases in mk_num, dest_num
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 20:33:52 -0700 |
huffman |
add semiring_assoc_fold simproc for unsigned numerals
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:57:16 -0700 |
huffman |
reorient simproc for unsigned numerals
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 15:14:31 -0700 |
huffman |
add more lemmas for signed comparisons
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 08:07:52 -0800 |
huffman |
add more ordering lemmas
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 20:45:23 -0800 |
huffman |
add lemmas for exponentiation
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 19:35:52 -0800 |
huffman |
tune section headings; add square function
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:42:45 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:42:15 -0800 |
huffman |
rearrange subsections
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:14:36 -0800 |
huffman |
remove instances num::semiring and num::linorder
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:08:21 -0800 |
huffman |
datatype num = One | Dig0 num | Dig1 num
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 12:53:59 -0800 |
huffman |
replace 1::num with One; remove monoid_mult instance
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 19:53:20 -0800 |
huffman |
replace dec with double-and-decrement function
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:38:10 +0100 |
haftmann |
tuned texts
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 09:09:51 +0200 |
haftmann |
op = vs. eq
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|