src/HOL/Library/Float.thy
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
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-10 wenzelm 2012-10-10 eliminated some remaining uses of typedef with implicit set definition;
2012-05-16 kuncar 2012-05-16 generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-04-26 hoelzl 2012-04-26 add code equation for real_of_float
2012-04-20 hoelzl 2012-04-20 hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-19 hoelzl 2012-04-19 transfer now handles Let
2012-04-19 kuncar 2012-04-19 rename no_code to no_abs_code - more appropriate name
2012-04-19 hoelzl 2012-04-19 use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
2012-04-18 hoelzl 2012-04-18 use lifting to introduce floating point numbers
2012-04-18 hoelzl 2012-04-18 replace the float datatype by a type with unique representation
2012-03-30 wenzelm 2012-03-30 tuned proofs, less guesswork;
2012-03-27 huffman 2012-03-27 remove redundant lemmas
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
2012-02-21 wenzelm 2012-02-21 misc tuning; more indentation;
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-12-06 hoelzl 2011-12-06 tuned proofs
2011-11-14 hoelzl 2011-11-14 cleaned up float theories; removed duplicate definitions and theorems
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-05-04 wenzelm 2011-05-04 proper case_names for int_cases, int_of_nat_induct; tuned some proofs, eliminating (cases, auto) anti-pattern;
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2010-12-06 hoelzl 2010-12-06 move coercions to appropriate places
2010-09-06 hoelzl 2010-09-06 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-02-23 huffman 2010-02-23 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures