Commits · b574e6b58c93bd9dce8554990e3b9d2fc443bdbc · Flocq / flocq

01 Oct, 2010 4 commits
- Added COPYING file. · b574e6b5
  Guillaume Melquiond authored Oct 01, 2010
  
  b574e6b5
- Changed some theorem names. · 4aa79696
  Guillaume Melquiond authored Oct 01, 2010
  
  4aa79696
- Added implicit coercions for radix and ln_beta. · 81b2a74c
  Guillaume Melquiond authored Oct 01, 2010
  
  81b2a74c
- WIP pred(x) · fb5135b4
  BOLDO Sylvie authored Oct 01, 2010
  
  fb5135b4
29 Sep, 2010 3 commits
- Still about pred · 750219e4
  BOLDO Sylvie authored Sep 29, 2010
  
  750219e4
- rounding_DN_pred · f26588e6
  BOLDO Sylvie authored Sep 29, 2010
  
  f26588e6
- Req_bool + Fpred -> pred · 69a33aa7
  BOLDO Sylvie authored Sep 29, 2010
  
  69a33aa7
24 Sep, 2010 3 commits
- Fpred again · 6c9ae78e
  BOLDO Sylvie authored Sep 24, 2010
  
  6c9ae78e
- Fpred_ulp · e27596da
  BOLDO Sylvie authored Sep 24, 2010
  
  e27596da
- Fpred · da9e58b3
  BOLDO Sylvie authored Sep 24, 2010
  
  da9e58b3
23 Sep, 2010 3 commits
- Still WIP predecessor · 44d263fb
  BOLDO Sylvie authored Sep 23, 2010
  
  44d263fb
- WIP aboout the predecessor · 3e16e76c
  BOLDO Sylvie authored Sep 23, 2010
  
  3e16e76c
- I need the predecessor :-/ · 42118aed
  BOLDO Sylvie authored Sep 23, 2010
  
  42118aed
22 Sep, 2010 6 commits
- WIP version · 3d44b057
  BOLDO Sylvie authored Sep 22, 2010
  
  3d44b057
- succ_lt_le needed for axpy · 2f0e650e
  BOLDO Sylvie authored Sep 22, 2010
  
  2f0e650e
- Simplified proof a bit. · 6674dc21
  Guillaume Melquiond authored Sep 22, 2010
  
  6674dc21
- Finished proof of generic_format_succ. · f656259a
  Guillaume Melquiond authored Sep 22, 2010
  
  f656259a
- Added some theorems about scaled_mantissa. · c541aaa6
  Guillaume Melquiond authored Sep 22, 2010
  
  c541aaa6
- Renamed Rabs_le theorems and added lt versions. · b3e635ab
  Guillaume Melquiond authored Sep 22, 2010
  
  b3e635ab
21 Sep, 2010 8 commits
- Added theorem rounding_up_succ. · aa2517ea
  Guillaume Melquiond authored Sep 21, 2010
  
  aa2517ea
- Admitted theorem generic_format_succ. · 16c12aa9
  Guillaume Melquiond authored Sep 21, 2010
  
  16c12aa9
- Split rounding_DN_ulp. · 0a5366a7
  Guillaume Melquiond authored Sep 21, 2010
  
  0a5366a7
- Added theorem rounding_DN_ulp. · 545b51dd
  Guillaume Melquiond authored Sep 21, 2010
  
  545b51dd
- A little Axpy · fd74178e
  BOLDO Sylvie authored Sep 21, 2010
  
  fd74178e
- Name change · bb571876
  BOLDO Sylvie authored Sep 21, 2010
  
  bb571876
- First version of Axpy · 718b6d16
  BOLDO Sylvie authored Sep 21, 2010
  
  718b6d16
- Change of stating of canonic_exp_ge · 9c3fc6c4
  BOLDO Sylvie authored Sep 21, 2010
  
  9c3fc6c4
20 Sep, 2010 1 commit
- canonic_exp_ge made more generic · b3738592
  BOLDO Sylvie authored Sep 20, 2010
  
  b3738592
17 Sep, 2010 8 commits
- Simplified proofs. · 68a4fd29
  Guillaume Melquiond authored Sep 17, 2010
  
  68a4fd29
- Added lemma Fexp_Fplus. Cleaned file along the way. · 96e32822
  Guillaume Melquiond authored Sep 17, 2010
  
  96e32822
- Simplified proof. · 9c381a88
  Guillaume Melquiond authored Sep 17, 2010
  
  9c381a88
- Weakened generic_format_plus. · 1e02a4ad
  Guillaume Melquiond authored Sep 17, 2010
  
  1e02a4ad
- Simplified proof. · b083def0
  Guillaume Melquiond authored Sep 17, 2010
  
  b083def0
- Added Zmin rewriting rules. · 615117eb
  Guillaume Melquiond authored Sep 17, 2010
  
  615117eb
- Added lemma generic_format_plus. · 2a8e1867
  Guillaume Melquiond authored Sep 17, 2010
  
  2a8e1867
- mult_error_FLT by clean translation · 3483f242
  BOLDO Sylvie authored Sep 17, 2010
  
  3483f242
16 Sep, 2010 4 commits
- Simplified proof a bit. · 21cf8f73
  Guillaume Melquiond authored Sep 16, 2010
  
  21cf8f73
- Simplified proof. · 3429e38d
  Guillaume Melquiond authored Sep 16, 2010
  
  3429e38d
- Removed useless hypothesis. · 64b09583
  Guillaume Melquiond authored Sep 16, 2010
  
  64b09583
- mult_error_FLT using translation from FLX · 88b27d10
  BOLDO Sylvie authored Sep 16, 2010
  
  88b27d10