| Thu, 10 Dec 2009 17:34:18 +0000 |
paulson |
streamlined proofs
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| 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
|
| Tue, 03 Feb 2009 11:16:28 +0100 |
krauss |
declare "nat o abs" as default measure for int
|
file |
diff |
annotate
|
| Sat, 31 Jan 2009 09:04:16 +0100 |
nipkow |
added some simp rules
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 12:31:35 -0800 |
huffman |
clean up diff_bin_simps
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 20:36:20 -0800 |
huffman |
separate neg_simps from rel_simps
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 16:28:09 -0800 |
huffman |
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 12:32:38 -0800 |
huffman |
add named lemma lists: neg_simps and iszero_simps
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 11:14:24 -0800 |
huffman |
change arith_special simps to avoid using neg
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 21:50:36 -0800 |
huffman |
enable eq_bin_simps for simplifying equalities on numerals
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 20:45:42 -0800 |
huffman |
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 14:23:03 -0800 |
huffman |
cleaned up subsection headings;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 08:18:56 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:43 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 08:47:27 +0200 |
haftmann |
established canonical argument order in SML code generators
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:18 +0200 |
haftmann |
tuned of_nat code generation
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 10:17:22 +0200 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 13:41:28 +0200 |
haftmann |
code generator setup for "int" also works under eta-contraction
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Fri, 23 May 2008 16:41:39 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
file |
diff |
annotate
|