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
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