Commits · 69e7e6593313c7c37c75498afece65ca00069f98 · Flocq / flocq

05 Oct, 2010 1 commit
- More comments (and used by coqdoc) · a90ca0c2
  BOLDO Sylvie authored Oct 05, 2010
  
  a90ca0c2
01 Oct, 2010 2 commits
- Added license banner to the .v files. · ec58e33a
  Guillaume Melquiond authored Oct 01, 2010
  
  ec58e33a
- Changed some theorem names. · 4aa79696
  Guillaume Melquiond authored Oct 01, 2010
  
  4aa79696
02 Sep, 2010 1 commit
- Removed almost empty file. · 40982267
  Guillaume Melquiond authored Sep 02, 2010
  
  40982267
17 May, 2010 2 commits
- Moved opposites to goals. · 39cf7e2e
  Guillaume Melquiond authored May 17, 2010
  
  39cf7e2e
- Added Rnd_{DN,UP}_pt_N. · 16cf11e2
  Guillaume Melquiond authored May 17, 2010
  
  16cf11e2
11 May, 2010 1 commit
- Added Rnd_N_pt_unicity. · 6e4f4e8d
  Guillaume Melquiond authored May 11, 2010
  
  6e4f4e8d
13 Apr, 2010 1 commit
- Added lemma Rnd_DN_UP_pt_N. · 23cf3d6e
  Guillaume Melquiond authored Apr 13, 2010
  
  23cf3d6e
02 Mar, 2010 1 commit
- Added Rnd_NG_pt_refl. · 2f757e26
  Guillaume Melquiond authored Mar 02, 2010
  
  2f757e26
24 Feb, 2010 2 commits
- Added splitting around rounding bounds. · c04b5ef9
  Guillaume Melquiond authored Feb 24, 2010
  
  c04b5ef9
- Refactored file hierarchy. · 12ff1621
  Guillaume Melquiond authored Feb 24, 2010
  
  12ff1621
04 Feb, 2010 1 commit
- Finished proof of DN_UP_parity_FLT_pos. · bdd4d892
  Guillaume Melquiond authored Feb 04, 2010
  
  bdd4d892
02 Nov, 2009 1 commit
- Linked monotony and location respective to zero. · 4f6e8b1e
  Guillaume Melquiond authored Nov 02, 2009
  
  4f6e8b1e
30 Oct, 2009 2 commits
- Moved to rounding predicates. Simplified proofs. · e9dfd4d4
  Guillaume Melquiond authored Oct 30, 2009
  
  e9dfd4d4
- Added theorems about reflexivity of standard predicates. · 1574e8c2
  Guillaume Melquiond authored Oct 30, 2009
  
  1574e8c2
29 Oct, 2009 5 commits
- Proved Rnd_ZR_pt_monotone and satisfies_any_imp_ZR. · c8016fa9
  Guillaume Melquiond authored Oct 29, 2009
  
  c8016fa9
- Factored proofs a bit. · 1a041014
  Guillaume Melquiond authored Oct 29, 2009
  
  1a041014
- Added definitions for rounding predicates and extraction from them. · 7a9b8478
  Guillaume Melquiond authored Oct 29, 2009
  
  7a9b8478
- Gave a proper name and place to theorem toto. · 97b1ddd9
  Guillaume Melquiond authored Oct 29, 2009
  
  97b1ddd9
- Changed epow to bpow, Lemma to Theorem, Rabs_Z2R to abs_Z2R. · 416d16fe
  Guillaume Melquiond authored Oct 29, 2009
  
  416d16fe
07 Oct, 2009 1 commit
- Merged Rnd_N1 and Rnd_N2 into Rnd_NG. · 3106df88
  Guillaume Melquiond authored Oct 07, 2009
  
  3106df88
24 Sep, 2009 1 commit
- Generalized definition of rounding to nearest. · e5dfbe02
  Guillaume Melquiond authored Sep 24, 2009
  
  e5dfbe02
18 Sep, 2009 1 commit
- Added intermediate lemma for DN_or_UP. · 6d7a279c
  Guillaume Melquiond authored Sep 18, 2009
  
  6d7a279c
16 Sep, 2009 1 commit
- Changed NE to generic NE (abs-based) and finished proof. · c146b544
  Guillaume Melquiond authored Sep 16, 2009
  
  c146b544
15 Sep, 2009 1 commit
- Started proofs on rounding to nearest even. · 6bbe7159
  Guillaume Melquiond authored Sep 15, 2009
  
  6bbe7159
08 Apr, 2009 1 commit
- Added Rnd_UP_DN_pt_sym. · d9c585fa
  Guillaume Melquiond authored Apr 08, 2009
  
  d9c585fa
23 Jan, 2009 1 commit
- Split properties. · 20b97dd0
  Guillaume Melquiond authored Jan 23, 2009
  
  20b97dd0