| Wed, 14 Jul 2010 16:13:14 +0200 |
haftmann |
avoid export_code ... file -
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:32:14 +0100 |
wenzelm |
adapted to authentic syntax -- actual types are verbatim;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:17:33 +0100 |
wenzelm |
explicit @{type_syntax} markup;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:19:58 +0100 |
wenzelm |
modernized translations;
|
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
|
| Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:17:35 +0100 |
wenzelm |
recovered from 7a1f597f454e, simplified imports;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 08:14:23 +0100 |
haftmann |
adjusted import to changed HOL theory graph
|
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
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| 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
|