src/HOL/Library/Float.thy
20 months ago immler 2018-02-05 added lemmas, avoid 'float_of 0'
21 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
22 months ago haftmann 2017-12-02 more simplification rules
23 months ago immler 2017-10-24 generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2017-03-05 nipkow 2017-03-05 added numeral_powr_numeral
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 more standardized names
2016-08-12 nipkow 2016-08-12 tuned
2016-08-12 nipkow 2016-08-12 Extracted floorlog and bitlen to separate theory Log_Nat
2016-08-05 nipkow 2016-08-05 fixed floor proofs
2016-08-05 nipkow 2016-08-05 more lemmas
2016-06-24 wenzelm 2016-06-24 misc tuning and modernization;
2016-06-08 immler 2016-06-08 generalized bitlen to floor of log
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-26 immler 2016-02-26 finite precision computation to determine sign for comparison
2016-02-26 immler 2016-02-26 positive precision for truncate; fixed precision for approximation of rationals; code for truncate
2016-02-26 immler 2016-02-26 compute_real_of_float has not been used as code equation
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-11 paulson 2015-11-11 new conversion theorems for int, nat to float
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-07-09 wenzelm 2015-07-09 tuned proofs;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-07 wenzelm 2015-06-07 tuned;
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-04-09 haftmann 2015-04-09 conversion between division on nat/int and division in archmedean fields
2015-02-18 haftmann 2015-02-18 inlined rules to free user-space from technical names
2015-02-06 haftmann 2015-02-06 default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-11-12 immler 2014-11-12 tuned proofs
2014-11-12 immler 2014-11-12 quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
2014-11-12 immler 2014-11-12 truncate intermediate results in horner to improve performance of approximate; more efficient truncated addition float_plus_up/float_plus_down
2014-11-12 immler 2014-11-12 simplified computations based on round_up by reducing to round_down; more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-08-25 hoelzl 2014-08-25 introduce real_of typeclass for real :: 'a => real
2014-08-05 wenzelm 2014-08-05 tuned proofs;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-04-28 wenzelm 2014-04-28 tuned;
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2013-12-16 immler 2013-12-16 monotonicity of rounding and truncating float
2013-12-16 immler 2013-12-16 Float: prevent unnecessary large numbers when adding 0
2013-12-16 immler 2013-12-16 additional definitions and lemmas for Float
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus