| Thu, 29 Oct 2009 22:13:11 +0100 |
haftmann |
moved some dvd [int] facts to Int
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:38 +0100 |
haftmann |
moved some dvd [int] facts to 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
|
| Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:15:59 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
added numeral code postprocessor rules on type int
|
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
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Fri, 08 May 2009 08:00:11 +0200 |
haftmann |
moved int_factor_simprocs.ML to theory Int
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:15:01 -0700 |
huffman |
reimplement reorientation simproc using theory data
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:29 +0200 |
haftmann |
reorganization of power lemmas
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 13:34:46 +0200 |
haftmann |
local syntax for Ints; ephermal re-globalization
|
file |
diff |
annotate
|
| Mon, 27 Apr 2009 10:11:44 +0200 |
haftmann |
cleaned up theory power further
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 22:29:10 +0200 |
nipkow |
cleaned up setprod_zero-related lemmas
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 16:55:31 +0200 |
nipkow |
added setsum_pos_nat
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 12:07:59 -0700 |
huffman |
simplify theorem references
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 10:47:41 -0700 |
huffman |
no longer delay loading of assoc_fold.ML
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:10 +0100 |
haftmann |
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
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, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 16:25:52 -0800 |
huffman |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 18:16:19 -0800 |
huffman |
declare of_int_number_of_eq [simp]
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 20:33:23 +0100 |
blanchet |
Added Nitpick tag to 'of_int_of_nat'.
|
file |
diff |
annotate
|