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