| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-01 |
nipkow |
2009-03-01 |
removed redundant lemmas
|
file | diff | annotate |
| 2009-03-01 |
nipkow |
2009-03-01 |
added lemmas by Jeremy Avigad
|
file | diff | annotate |
| 2009-02-23 |
huffman |
2009-02-23 |
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 |
| 2009-02-21 |
nipkow |
2009-02-21 |
Removed subsumed lemmas
|
file | diff | annotate |
| 2009-02-21 |
nipkow |
2009-02-21 |
removed redundant thms
|
file | diff | annotate |
| 2009-02-20 |
nipkow |
2009-02-20 |
Removed redundant lemmas
|
file | diff | annotate |
| 2009-02-18 |
huffman |
2009-02-18 |
generalize int_dvd_cancel_factor simproc to idom class
|
file | diff | annotate |
| 2009-02-17 |
huffman |
2009-02-17 |
merged
|
file | diff | annotate |
| 2009-02-17 |
huffman |
2009-02-17 |
remove redundant simp attributes for zdvd rules
|
file | diff | annotate |
| 2009-02-17 |
nipkow |
2009-02-17 |
Cleaned up IntDiv and removed subsumed lemmas.
|
file | diff | annotate |
| 2009-02-16 |
haftmann |
2009-02-16 |
added pdivmod on int (for code generation)
|
file | diff | annotate |
| 2009-01-31 |
nipkow |
2009-01-31 |
added some simp rules
|
file | diff | annotate |
| 2009-01-28 |
nipkow |
2009-01-28 |
merged - resolving conflics
|
file | diff | annotate |
| 2009-01-28 |
nipkow |
2009-01-28 |
Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now
|
file | diff | annotate |
| 2009-01-28 |
haftmann |
2009-01-28 |
slightly adapted towards more uniformity with div/mod on nat
|
file | diff | annotate |
| 2009-01-08 |
huffman |
2009-01-08 |
remove type-specific proofs
|
file | diff | annotate |
| 2009-01-08 |
huffman |
2009-01-08 |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
file | diff | annotate |
| 2009-01-08 |
huffman |
2009-01-08 |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
file | diff | annotate |
| 2009-01-08 |
huffman |
2009-01-08 |
generalize some div/mod lemmas; remove type-specific proofs
|
file | diff | annotate |
| 2008-12-10 |
huffman |
2008-12-10 |
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
|
file | diff | annotate |
| 2008-10-10 |
haftmann |
2008-10-10 |
`code func` now just `code`
|
file | diff | annotate |
| 2008-09-17 |
wenzelm |
2008-09-17 |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file | diff | annotate |
| 2008-07-21 |
chaieb |
2008-07-21 |
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
|
file | diff | annotate |
| 2008-07-18 |
haftmann |
2008-07-18 |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file | diff | annotate |
| 2008-04-02 |
haftmann |
2008-04-02 |
moved some code lemmas for Numerals here
|
file | diff | annotate |
| 2008-03-29 |
wenzelm |
2008-03-29 |
replaced 'ML_setup' by 'ML';
|
file | diff | annotate |
| 2008-02-20 |
haftmann |
2008-02-20 |
tuned structures in arith_data.ML
|
file | diff | annotate |
| 2008-02-17 |
huffman |
2008-02-17 |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file | diff | annotate |
| 2008-01-25 |
haftmann |
2008-01-25 |
moved definition of power on ints to theory Int
|
file | diff | annotate |
| 2008-01-22 |
haftmann |
2008-01-22 |
added class semiring_div
|
file | diff | annotate |
| 2008-01-15 |
haftmann |
2008-01-15 |
joined theories IntDef, Numeral, IntArith to theory Int
|
file | diff | annotate |
| 2007-12-07 |
haftmann |
2007-12-07 |
instantiation target rather than legacy instance
|
file | diff | annotate |
| 2007-10-21 |
nipkow |
2007-10-21 |
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.
|
file | diff | annotate |
| 2007-10-20 |
chaieb |
2007-10-20 |
fixed proofs
|
file | diff | annotate |
| 2007-10-12 |
haftmann |
2007-10-12 |
class div inherits from class times
|
file | diff | annotate |
| 2007-09-18 |
wenzelm |
2007-09-18 |
simplified type int (eliminated IntInf.int, integer);
|
file | diff | annotate |
| 2007-08-30 |
nipkow |
2007-08-30 |
added lemma
|
file | diff | annotate |
| 2007-08-30 |
huffman |
2007-08-30 |
ported div/mod simprocs from HOL/ex/Binary.thy
|
file | diff | annotate |
| 2007-08-21 |
huffman |
2007-08-21 |
add lemma of_int_power
|
file | diff | annotate |
| 2007-08-15 |
paulson |
2007-08-15 |
ATP blacklisting is now in theory data, attribute noatp
|
file | diff | annotate |
| 2007-08-09 |
haftmann |
2007-08-09 |
tuned
|
file | diff | annotate |
| 2007-07-25 |
nipkow |
2007-07-25 |
Added lemmas
|
file | diff | annotate |
| 2007-07-24 |
nipkow |
2007-07-24 |
Added cancel simprocs for dvd on nat and int
|
file | diff | annotate |
| 2007-07-19 |
haftmann |
2007-07-19 |
added lemmas by Brian Huffman
|
file | diff | annotate |
| 2007-07-10 |
haftmann |
2007-07-10 |
introduced (auxiliary) class dvd_mod for more convenient code generation
|
file | diff | annotate |
| 2007-06-28 |
haftmann |
2007-06-28 |
code generation for dvd
|
file | diff | annotate |
| 2007-06-23 |
nipkow |
2007-06-23 |
tuned and renamed group_eq_simps and ring_eq_simps
|
file | diff | annotate |
| 2007-06-20 |
huffman |
2007-06-20 |
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 |
| 2007-06-16 |
nipkow |
2007-06-16 |
tuned
|
file | diff | annotate |
| 2007-06-13 |
huffman |
2007-06-13 |
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int
|
file | diff | annotate |
| 2007-06-11 |
huffman |
2007-06-11 |
modify proofs to avoid referring to int::nat=>int
|
file | diff | annotate |
| 2007-06-11 |
huffman |
2007-06-11 |
add int_of_nat versions of lemmas about int::nat=>int
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
moved Integ files to canonical place;
|
file | diff | annotate |