20081129 
nipkow 
20081129 
Floats for Real.

file  diff  annotate 
20081010 
haftmann 
20081010 
`code func` now just `code`

file  diff  annotate 
20081007 
haftmann 
20081007 
tuned code setup

file  diff  annotate 
20080925 
haftmann 
20080925 
non leftlinear equations for nbe

file  diff  annotate 
20080902 
nipkow 
20080902 
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
distributed them over Real/ (to do with bijections and density).
Library/NatPair became Nat_Int_Bij and made that part of Main.

file  diff  annotate 
20080826 
nipkow 
20080826 
Defined rationals (Rats) globally in Rational.
Chractarized them with a few lemmas in RealDef, one of them from Sqrt.

file  diff  annotate 
20080823 
nipkow 
20080823 
added const Rational
added more function puzzles

file  diff  annotate 
20080811 
haftmann 
20080811 
rudimentary code setup for set operations

file  diff  annotate 
20080725 
haftmann 
20080725 
added class preorder

file  diff  annotate 
20080721 
chaieb 
20080721 
Tuned and simplified proofs

file  diff  annotate 
20080718 
haftmann 
20080718 
refined code generator setup for rational numbers; more simplification rules for rational numbers

file  diff  annotate 
20080711 
haftmann 
20080711 
improved code generator setup

file  diff  annotate 
20080610 
haftmann 
20080610 
removed some dubious code lemmas

file  diff  annotate 
20080422 
haftmann 
20080422 
constant HOL.eq now qualified

file  diff  annotate 
20080402 
haftmann 
20080402 
explicit class "eq" for operational equality

file  diff  annotate 
20080125 
haftmann 
20080125 
improved code theorem setup

file  diff  annotate 
20080110 
berghofe 
20080110 
New interface for test data generators.

file  diff  annotate 
20080102 
haftmann 
20080102 
splitted class uminus from class minus

file  diff  annotate 
20071207 
haftmann 
20071207 
instantiation target rather than legacy instance

file  diff  annotate 
20071205 
obua 
20071205 
instance int,real :: lordered_ring

file  diff  annotate 
20071129 
haftmann 
20071129 
instance command as rudimentary class target

file  diff  annotate 
20071106 
haftmann 
20071106 
renamed lordered_*_* to lordered_*_add_*; further localization

file  diff  annotate 
20071023 
nipkow 
20071023 
went back to >0

file  diff  annotate 
20071021 
nipkow 
20071021 
More changes from >0 to ~=0::nat

file  diff  annotate 
20071021 
nipkow 
20071021 
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

file  diff  annotate 
20071020 
chaieb 
20071020 
fixed proofs

file  diff  annotate 
20070918 
wenzelm 
20070918 
simplified type int (eliminated IntInf.int, integer);

file  diff  annotate 
20070918 
haftmann 
20070918 
renamed constructor RealC to Ratreal

file  diff  annotate 
20070906 
berghofe 
20070906 
New code generator setup (taken from Library/Executable_Real.thy,
also works for old code generator).

file  diff  annotate 
20070901 
nipkow 
20070901 
final(?) iteration of sgn saga.

file  diff  annotate 
20070809 
haftmann 
20070809 
adaptions for code generation

file  diff  annotate 
20070731 
wenzelm 
20070731 
arith method setup: proper context;

file  diff  annotate 
20070720 
haftmann 
20070720 
split class abs from class minus

file  diff  annotate 
20070624 
nipkow 
20070624 
tuned and used field_simps

file  diff  annotate 
20070623 
nipkow 
20070623 
tuned and renamed group_eq_simps and ring_eq_simps

file  diff  annotate 
20070620 
huffman 
20070620 
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int

file  diff  annotate 
20070620 
huffman 
20070620 
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 
20070607 
huffman 
20070607 
remove redundant lemmas

file  diff  annotate 
20070607 
huffman 
20070607 
remove references to prealspecific theorems

file  diff  annotate 
20070607 
huffman 
20070607 
define (1::preal); clean up instance declarations

file  diff  annotate 
20070519 
nipkow 
20070519 
added code generation based on Isabelle's rat type.

file  diff  annotate 
20070514 
huffman 
20070514 
move lemmas to RealPow.thy; tuned proofs

file  diff  annotate 
20070514 
huffman 
20070514 
remove redundant lemmas

file  diff  annotate 
20070514 
huffman 
20070514 
cleaned up

file  diff  annotate 
20070316 
haftmann 
20070316 
added lattice definitions

file  diff  annotate 
20061117 
wenzelm 
20061117 
more robust syntax for definition/abbreviation/notation;

file  diff  annotate 
20060916 
huffman 
20060916 
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 
20060906 
haftmann 
20060906 
got rid of Numeral.bin type

file  diff  annotate 
20060726 
webertj 
20060726 
linear arithmetic splits certain operators (e.g. min, max, abs)

file  diff  annotate 
20060602 
wenzelm 
20060602 
misc cleanup;

file  diff  annotate 
20060212 
kleing 
20060212 
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
* add nondenumerability 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 
20050801 
wenzelm 
20050801 
simprocs: Simplifier.inherit_bounds;

file  diff  annotate 
20050719 
avigad 
20050719 
added list of theorem changes to NEWS
added real_of_int_abs to RealDef.thy

file  diff  annotate 
20050713 
avigad 
20050713 
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 
20050617 
haftmann 
20050617 
migrated theory headers to new format

file  diff  annotate 
20050504 
nipkow 
20050504 
fixed lin.arith

file  diff  annotate 
20050221 
nipkow 
20050221 
more fine tuniung

file  diff  annotate 
20041005 
paulson 
20041005 
new simprules for abs and for things like a/b<1

file  diff  annotate 
20040901 
paulson 
20040901 
new "respects" syntax for quotienting

file  diff  annotate 
20040818 
nipkow 
20040818 
import > imports

file  diff  annotate 