src/HOL/RealDef.thy
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
2013-02-19 kuncar 2013-02-19 delete also predicates on relations when hiding an implementation of an abstract type
2013-02-15 traytel 2013-02-15 Backed out changeset: 3fe7242f8346, many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets
2013-02-15 traytel 2013-02-15 coercions between base types can be lifted to sets
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-05-10 huffman 2012-05-10 convert real number theory to use lifting/transfer
2012-05-07 huffman 2012-05-07 tuned ordering of lemmas
2012-04-18 hoelzl 2012-04-18 add lemmas to remove real conversions when compared to power of numerals
2012-04-18 hoelzl 2012-04-18 add simp rules to rewrite comparisons of 1 and real
2012-04-16 huffman 2012-04-16 tuned some proofs; removed duplicate lemma zero_le_imp_of_nat
2012-04-12 huffman 2012-04-12 remove outdated comment
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-12-14 blanchet 2011-12-14 fixed Nitpick definition of "<" on "real"s
2011-12-12 bulwahn 2011-12-12 hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for real numbers; tuned
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-07 huffman 2011-09-07 remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-08-20 huffman 2011-08-20 replace lemma realpow_two_diff with new lemma square_diff_square_factored
2011-08-20 huffman 2011-08-20 remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-20 huffman 2011-08-20 move lemma add_eq_0_iff to Groups.thy
2011-08-20 huffman 2011-08-20 remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
2011-08-20 huffman 2011-08-20 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
2011-08-20 huffman 2011-08-20 remove some over-specific rules from the simpset
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-07-18 bulwahn 2011-07-18 adding narrowing instances for real and rational
2011-07-09 bulwahn 2011-07-09 adding code equations to execute floor and ceiling on rational and real numbers
2011-07-09 bulwahn 2011-07-09 adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
2011-04-08 bulwahn 2011-04-08 rational and real instances for new compilation scheme for exhaustive quickcheck
2011-03-25 noschinl 2011-03-25 Change coercion for RealDef to use function application (not composition)
2011-03-11 bulwahn 2011-03-11 moving exhaustive_generators.ML to Quickcheck directory
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-17 bulwahn 2010-12-17 adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
2010-12-06 hoelzl 2010-12-06 move coercions to appropriate places
2010-12-06 nipkow 2010-12-06 moved coercion decl. for int
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 nipkow 2010-12-01 moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.
2010-11-30 haftmann 2010-11-30 merged
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent2 by plain definition
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent by plain definition
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
2010-11-30 huffman 2010-11-30 use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-09 blanchet 2010-08-09 replace "setup" with "declaration"
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-06-11 blanchet 2010-06-11 adjust Nitpick's handling of "<" on "rat"s and "reals"
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-15 huffman 2010-05-15 add real_le_linear to list of legacy theorem names
2010-05-11 huffman 2010-05-11 no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-10 huffman 2010-05-10 add real_mult_commute to legacy theorem names
2010-05-10 huffman 2010-05-10 new construction of real numbers using Cauchy sequences
2010-05-09 huffman 2010-05-09 remove a couple of redundant lemmas; simplify some proofs
2010-04-27 haftmann 2010-04-27 tuned class linordered_field_inverse_zero