| Wed, 30 May 2012 14:55:44 +0200 |
huffman |
remove unnecessary simp rules involving Abs_Integ
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 16:44:23 +0200 |
huffman |
load Tools/numeral.ML in Num.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 15:56:12 +0200 |
huffman |
set up numeral reorient simproc in Num.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:10:28 +0200 |
huffman |
move lemmas from Nat_Numeral to Int.thy and Num.thy
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 14:09:10 +0200 |
huffman |
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 02 Mar 2012 09:35:32 +0100 |
bulwahn |
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 06:04:59 +0100 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 06:01:47 +0100 |
huffman |
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
|
file |
diff |
annotate
|
| Thu, 20 Oct 2011 17:27:14 +0200 |
huffman |
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 15:42:43 +0200 |
wenzelm |
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:26 +0200 |
bulwahn |
removing old code generator setup for integers
|
file |
diff |
annotate
|
| Sun, 09 Oct 2011 11:13:53 +0200 |
huffman |
Int.thy: discontinued some legacy theorems
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 07:15:13 -0700 |
huffman |
introduce abbreviation 'int' earlier in Int.thy
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 06:27:59 -0700 |
huffman |
move lemmas nat_le_iff and nat_mono into Int.thy
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 16:00:09 -0700 |
huffman |
remove duplicate lemma nat_zero in favor of nat_0
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 09:04:20 -0700 |
huffman |
added number_semiring class, plus a few new lemmas;
|
file |
diff |
annotate
|
| Wed, 04 May 2011 15:37:39 +0200 |
wenzelm |
proper case_names for int_cases, int_of_nat_induct;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 15:58:09 +0100 |
haftmann |
adapted proofs to slightly changed definitions of congruent(2)
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 11 May 2010 08:36:02 +0200 |
haftmann |
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:55:04 +0200 |
haftmann |
moved int induction lemma to theory Int as int_bidirectional_induct
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:51:55 +0200 |
haftmann |
moved lemma zdvd_period to theory Int
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:56 +0200 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| Thu, 06 May 2010 18:16:07 +0200 |
haftmann |
moved generic lemmas to appropriate places
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 12:20:09 +0200 |
haftmann |
got rid of [simplified]
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
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
|
| Tue, 06 Apr 2010 10:46:28 +0200 |
boehmes |
added missing mult_1_left to linarith simp rules
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:14:54 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 08:40:38 -0800 |
huffman |
add more simp rules for Ints
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Sat, 13 Feb 2010 23:24:57 +0100 |
wenzelm |
modernized structures;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
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, 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
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:26 +0200 |
haftmann |
moved some code lemmas for Numerals here
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
| Sat, 16 Feb 2008 02:01:13 +0100 |
huffman |
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:53:52 +0100 |
haftmann |
moved definition of power on ints to theory Int
|
file |
diff |
annotate
|
| Mon, 21 Jan 2008 08:43:27 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|