| 2008-01-10 |
berghofe |
2008-01-10 |
New interface for test data generators.
|
file | diff | annotate |
| 2008-01-02 |
haftmann |
2008-01-02 |
splitted class uminus from class minus
|
file | diff | annotate |
| 2007-12-07 |
haftmann |
2007-12-07 |
instantiation target rather than legacy instance
|
file | diff | annotate |
| 2007-12-05 |
obua |
2007-12-05 |
instance int,real :: lordered_ring
|
file | diff | annotate |
| 2007-11-29 |
haftmann |
2007-11-29 |
instance command as rudimentary class target
|
file | diff | annotate |
| 2007-11-06 |
haftmann |
2007-11-06 |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file | diff | annotate |
| 2007-10-23 |
nipkow |
2007-10-23 |
went back to >0
|
file | diff | annotate |
| 2007-10-21 |
nipkow |
2007-10-21 |
More changes from >0 to ~=0::nat
|
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-09-18 |
wenzelm |
2007-09-18 |
simplified type int (eliminated IntInf.int, integer);
|
file | diff | annotate |
| 2007-09-18 |
haftmann |
2007-09-18 |
renamed constructor RealC to Ratreal
|
file | diff | annotate |
| 2007-09-06 |
berghofe |
2007-09-06 |
New code generator setup (taken from Library/Executable_Real.thy,
also works for old code generator).
|
file | diff | annotate |
| 2007-09-01 |
nipkow |
2007-09-01 |
final(?) iteration of sgn saga.
|
file | diff | annotate |
| 2007-08-09 |
haftmann |
2007-08-09 |
adaptions for code generation
|
file | diff | annotate |
| 2007-07-31 |
wenzelm |
2007-07-31 |
arith method setup: proper context;
|
file | diff | annotate |
| 2007-07-20 |
haftmann |
2007-07-20 |
split class abs from class minus
|
file | diff | annotate |
| 2007-06-24 |
nipkow |
2007-06-24 |
tuned and used field_simps
|
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 |
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
|
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-07 |
huffman |
2007-06-07 |
remove redundant lemmas
|
file | diff | annotate |
| 2007-06-07 |
huffman |
2007-06-07 |
remove references to preal-specific theorems
|
file | diff | annotate |
| 2007-06-07 |
huffman |
2007-06-07 |
define (1::preal); clean up instance declarations
|
file | diff | annotate |
| 2007-05-19 |
nipkow |
2007-05-19 |
added code generation based on Isabelle's rat type.
|
file | diff | annotate |
| 2007-05-14 |
huffman |
2007-05-14 |
move lemmas to RealPow.thy; tuned proofs
|
file | diff | annotate |
| 2007-05-14 |
huffman |
2007-05-14 |
remove redundant lemmas
|
file | diff | annotate |
| 2007-05-14 |
huffman |
2007-05-14 |
cleaned up
|
file | diff | annotate |
| 2007-03-16 |
haftmann |
2007-03-16 |
added lattice definitions
|
file | diff | annotate |
| 2006-11-17 |
wenzelm |
2006-11-17 |
more robust syntax for definition/abbreviation/notation;
|
file | diff | annotate |
| 2006-09-16 |
huffman |
2006-09-16 |
define new constant of_real for class real_algebra_1;
define set Reals as range of_real;
add lemmas about of_real and Reals
|
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-06-02 |
wenzelm |
2006-06-02 |
misc cleanup;
|
file | diff | annotate |
| 2006-02-12 |
kleing |
2006-02-12 |
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
* add non-denumerability of continuum in Real, includes closed intervals on real
(contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)
|
file | diff | annotate |
| 2005-08-01 |
wenzelm |
2005-08-01 |
simprocs: Simplifier.inherit_bounds;
|
file | diff | annotate |
| 2005-07-19 |
avigad |
2005-07-19 |
added list of theorem changes to NEWS
added real_of_int_abs to RealDef.thy
|
file | diff | annotate |
| 2005-07-13 |
avigad |
2005-07-13 |
Additions to the Real (and Hyperreal) libraries:
RealDef.thy: lemmas relating nats, ints, and reals
reversed direction of real_of_int_mult, etc. (now they agree with nat versions)
SEQ.thy and Series.thy: various additions
RComplete.thy: lemmas involving floor and ceiling
introduced natfloor and natceiling
Log.thy: various additions
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2005-05-04 |
nipkow |
2005-05-04 |
fixed lin.arith
|
file | diff | annotate |
| 2005-02-21 |
nipkow |
2005-02-21 |
more fine tuniung
|
file | diff | annotate |
| 2004-10-05 |
paulson |
2004-10-05 |
new simprules for abs and for things like a/b<1
|
file | diff | annotate |
| 2004-09-01 |
paulson |
2004-09-01 |
new "respects" syntax for quotienting
|
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-29 |
paulson |
2004-07-29 |
removal of more iff-rules from RealDef.thy
|
file | diff | annotate |
| 2004-07-29 |
paulson |
2004-07-29 |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file | diff | annotate |
| 2004-07-26 |
paulson |
2004-07-26 |
converting Hyperreal/Transcendental to Isar script
|
file | diff | annotate |
| 2004-07-01 |
paulson |
2004-07-01 |
new treatment of binary numerals
|
file | diff | annotate |
| 2004-06-24 |
paulson |
2004-06-24 |
replaced monomorphic abs definitions by abs_if
|
file | diff | annotate |
| 2004-05-18 |
obua |
2004-05-18 |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file | diff | annotate |
| 2004-05-11 |
obua |
2004-05-11 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| 2004-05-01 |
wenzelm |
2004-05-01 |
tuned instance statements;
|
file | diff | annotate |
| 2004-04-23 |
paulson |
2004-04-23 |
congruent2 now allows different equiv relations
|
file | diff | annotate |
| 2004-03-30 |
paulson |
2004-03-30 |
tidied
|
file | diff | annotate |
| 2004-03-25 |
paulson |
2004-03-25 |
new treatment of equivalence classes
|
file | diff | annotate |
| 2004-03-19 |
paulson |
2004-03-19 |
removed redundant thms
|
file | diff | annotate |
| 2004-03-08 |
paulson |
2004-03-08 |
generic theorems about exponentials; general tidying up
|
file | diff | annotate |
| 2004-03-04 |
paulson |
2004-03-04 |
new material from Avigad, and simplified treatment of division by 0
|
file | diff | annotate |
| 2004-03-02 |
paulson |
2004-03-02 |
fixed bugs in the setup of arithmetic procedures
|
file | diff | annotate |