| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-02-20 |
nipkow |
2009-02-20 |
Removed redundant lemmas
|
file | diff | annotate |
| 2009-02-20 |
nipkow |
2009-02-20 |
removed subsumed lemmas
|
file | diff | annotate |
| 2009-02-02 |
haftmann |
2009-02-02 |
dropped Id
|
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 |
| 2008-12-03 |
huffman |
2008-12-03 |
enable eq_bin_simps for simplifying equalities on numerals
|
file | diff | annotate |
| 2008-09-29 |
haftmann |
2008-09-29 |
clarified dependencies between arith tools
|
file | diff | annotate |
| 2008-09-18 |
wenzelm |
2008-09-18 |
simplified oracle interface;
|
file | diff | annotate |
| 2008-07-21 |
chaieb |
2008-07-21 |
Tuned and simplified proofs
|
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-07-11 |
haftmann |
2008-07-11 |
separate class dvd for divisibility predicate
|
file | diff | annotate |
| 2008-04-02 |
haftmann |
2008-04-02 |
moved some code lemmas for Numerals to other theories
|
file | diff | annotate |
| 2008-02-27 |
chaieb |
2008-02-27 |
loads Tools/Qelim/qelim.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-02-16 |
huffman |
2008-02-16 |
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
|
file | diff | annotate |
| 2008-01-15 |
haftmann |
2008-01-15 |
joined theories IntDef, Numeral, IntArith to theory Int
|
file | diff | annotate |
| 2007-10-30 |
haftmann |
2007-10-30 |
continued localization
|
file | diff | annotate |
| 2007-10-12 |
haftmann |
2007-10-12 |
class div inherits from class times
|
file | diff | annotate |
| 2007-08-22 |
chaieb |
2007-08-22 |
tuned;
|
file | diff | annotate |
| 2007-07-31 |
wenzelm |
2007-07-31 |
proper context for cooper_tac within arith;
|
file | diff | annotate |
| 2007-07-31 |
wenzelm |
2007-07-31 |
arith method setup: proper context;
|
file | diff | annotate |
| 2007-07-19 |
haftmann |
2007-07-19 |
code lemma for of_int
|
file | diff | annotate |
| 2007-07-10 |
haftmann |
2007-07-10 |
moved lemma zdvd_period here
|
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-21 |
huffman |
2007-06-21 |
section headings
|
file | diff | annotate |
| 2007-06-21 |
wenzelm |
2007-06-21 |
moved Presburger setup back to Presburger.thy;
|
file | diff | annotate |
| 2007-06-21 |
wenzelm |
2007-06-21 |
adapted tool setup;
|
file | diff | annotate |
| 2007-06-20 |
huffman |
2007-06-20 |
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
|
file | diff | annotate |
| 2007-06-20 |
huffman |
2007-06-20 |
section headings
|
file | diff | annotate |
| 2007-06-17 |
chaieb |
2007-06-17 |
moved lemma all_not_ex to HOL.thy ; tuned proofs
|
file | diff | annotate |
| 2007-06-14 |
chaieb |
2007-06-14 |
Added some lemmas to default presburger simpset; tuned proofs
|
file | diff | annotate |
| 2007-06-14 |
wenzelm |
2007-06-14 |
tuned proofs: avoid implicit prems;
|
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-12 |
chaieb |
2007-06-12 |
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
|
file | diff | annotate |
| 2007-06-11 |
chaieb |
2007-06-11 |
A new and cleaned up Theory for QE. for Presburger arithmetic
|
file | diff | annotate |
| 2007-06-05 |
wenzelm |
2007-06-05 |
tuned comments;
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
moved Integ files to canonical place;
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
fixed title;
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
moved Integ files to canonical place;
|
file | diff | annotate |
| 2007-04-26 |
haftmann |
2007-04-26 |
cleaned up code generator setup for int
|
file | diff | annotate |
| 2007-04-20 |
haftmann |
2007-04-20 |
Isar definitions are now added explicitly to code theorem table
|
file | diff | annotate |
| 2007-03-02 |
haftmann |
2007-03-02 |
tuned code theorems for ord on integers
|
file | diff | annotate |
| 2007-01-06 |
chaieb |
2007-01-06 |
A few theorems on integer divisibily.
|
file | diff | annotate |
| 2006-11-22 |
haftmann |
2006-11-22 |
dropped eq const
|
file | diff | annotate |
| 2006-10-16 |
haftmann |
2006-10-16 |
moved HOL code generator setup to Code_Generator
|
file | diff | annotate |
| 2006-09-19 |
haftmann |
2006-09-19 |
improved numeral handling for nbe
|
file | diff | annotate |
| 2006-09-06 |
haftmann |
2006-09-06 |
got rid of Numeral.bin type
|
file | diff | annotate |
| 2006-07-26 |
webertj |
2006-07-26 |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file | diff | annotate |
| 2006-07-08 |
wenzelm |
2006-07-08 |
tuned;
|
file | diff | annotate |
| 2005-11-18 |
chaieb |
2005-11-18 |
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
|
file | diff | annotate |
| 2005-09-22 |
nipkow |
2005-09-22 |
renamed rules to iprover
|
file | diff | annotate |
| 2005-09-14 |
chaieb |
2005-09-14 |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
comm_ring : a reflected Method for proving equalities in a commutative ring
|
file | diff | annotate |
| 2005-07-14 |
wenzelm |
2005-07-14 |
improved oracle setup;
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2004-08-18 |
nipkow |
2004-08-18 |
import -> imports
|
file | diff | annotate |
| 2004-08-16 |
nipkow |
2004-08-16 |
New theory header syntax.
|
file | diff | annotate |
| 2004-07-01 |
paulson |
2004-07-01 |
new treatment of binary numerals
|
file | diff | annotate |
| 2004-06-21 |
kleing |
2004-06-21 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| 2004-06-14 |
chaieb |
2004-06-14 |
Oracle corrected
|
file | diff | annotate |