| Sun, 01 Mar 2009 10:24:57 +0100 |
nipkow |
added lemmas by Jeremy Avigad
|
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
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 23:46:03 +0100 |
nipkow |
Removed redundant lemmas
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 15:01:53 -0800 |
huffman |
generalize int_dvd_cancel_factor simproc to idom class
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 10:52:55 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 07:13:29 -0800 |
huffman |
remove redundant simp attributes for zdvd rules
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 19:11:15 +0100 |
haftmann |
added pdivmod on int (for code generation)
|
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
|
| Wed, 28 Jan 2009 11:02:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 12:25:22 -0800 |
huffman |
remove type-specific proofs
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 09:12:29 -0800 |
huffman |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:36:16 -0800 |
huffman |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:24:08 -0800 |
huffman |
generalize some div/mod lemmas; remove type-specific proofs
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 07:52:54 -0800 |
huffman |
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 13:36:44 +0200 |
chaieb |
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:26 +0200 |
haftmann |
moved some code lemmas for Numerals here
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 14:52:38 +0100 |
haftmann |
tuned structures in arith_data.ML
|
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
|
| Fri, 25 Jan 2008 14:53:52 +0100 |
haftmann |
moved definition of power on ints to theory Int
|
file |
diff |
annotate
|
| Tue, 22 Jan 2008 23:07:21 +0100 |
haftmann |
added class semiring_div
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 21:43:08 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 05:01:38 +0200 |
huffman |
ported div/mod simprocs from HOL/ex/Binary.thy
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 20:51:10 +0200 |
huffman |
add lemma of_int_power
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:45 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 18:10:28 +0200 |
nipkow |
Added lemmas
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 19:58:53 +0200 |
nipkow |
Added cancel simprocs for dvd on nat and int
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:38 +0200 |
haftmann |
added lemmas by Brian Huffman
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:10 +0200 |
haftmann |
introduced (auxiliary) class dvd_mod for more convenient code generation
|
file |
diff |
annotate
|
| Thu, 28 Jun 2007 19:09:34 +0200 |
haftmann |
code generation for dvd
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
| Sat, 16 Jun 2007 16:27:35 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 05:20:05 +0200 |
huffman |
modify proofs to avoid referring to int::nat=>int
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 02:25:55 +0200 |
huffman |
add int_of_nat versions of lemmas about int::nat=>int
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|