src/HOL/Library/Float.thy
2019-01-04 wenzelm isabelle update -u control_cartouches;
2018-09-24 nipkow Prefix form of infix with * on either side no longer needs special treatment
2018-06-07 nipkow utilize 'flip'
2018-02-05 immler added lemmas, avoid 'float_of 0'
2018-01-10 nipkow ran isabelle update_op on all sources
2017-12-02 haftmann more simplification rules
2017-10-24 immler 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 Further new material. The simprule status of some exp and ln identities was reverted.
2017-03-05 nipkow added numeral_powr_numeral
2016-10-16 haftmann eliminated irregular aliasses
2016-10-16 haftmann more standardized names
2016-08-12 nipkow tuned
2016-08-12 nipkow Extracted floorlog and bitlen to separate theory Log_Nat
2016-08-05 nipkow fixed floor proofs
2016-08-05 nipkow more lemmas
2016-06-24 wenzelm misc tuning and modernization;
2016-06-08 immler generalized bitlen to floor of log
2016-04-25 wenzelm eliminated old 'def';
2016-02-26 immler finite precision computation to determine sign for comparison
2016-02-26 immler positive precision for truncate; fixed precision for approximation of rationals; code for truncate
2016-02-26 immler compute_real_of_float has not been used as code equation
2016-02-23 nipkow more canonical names
2016-02-17 haftmann dropped various legacy fact bindings
2015-12-28 wenzelm more symbols;
2015-12-27 wenzelm prefer symbols for "floor", "ceiling";
2015-12-07 wenzelm isabelle update_cartouches -c -t;
2015-12-01 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-11 paulson new conversion theorems for int, nat to float
2015-11-10 paulson 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 direct bootstrap of integer division from natural division
2015-07-08 wenzelm tuned proofs;
2015-07-06 wenzelm tuned proofs;
2015-06-17 wenzelm isabelle update_cartouches;
2015-06-07 wenzelm tuned;
2015-04-11 paulson 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 conversion between division on nat/int and division in archmedean fields
2015-02-18 haftmann inlined rules to free user-space from technical names
2015-02-06 haftmann default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-11-12 immler tuned proofs
2014-11-12 immler quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
2014-11-12 immler truncate intermediate results in horner to improve performance of approximate;
2014-11-12 immler simplified computations based on round_up by reducing to round_down;
2014-11-02 wenzelm modernized header;
2014-10-30 haftmann more simp rules concerning dvd and even/odd
2014-09-21 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-08-25 hoelzl introduce real_of typeclass for real :: 'a => real
2014-08-05 wenzelm tuned proofs;
2014-07-04 haftmann reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell Hypsubst preserves equality hypotheses
2014-04-28 wenzelm tuned;
2014-04-14 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow made mult_pos_pos a simp rule
2014-04-11 nipkow made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-03-06 blanchet renamed 'fun_rel' to 'rel_fun'
2014-02-18 kuncar simplify proofs because of the stronger reflexivity prover
2013-12-16 immler monotonicity of rounding and truncating float
2013-12-16 immler Float: prevent unnecessary large numbers when adding 0
less more (0) -100 -60 tip