Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merge
  2. improved bisection algorithm for algebraic numbers
  3. added select_correct_factor_rat_poly as common factor+bisect algorithm
  4. soundness of select_correct_factor
  5. use BNF_Corec in Stern_Brocot
Changeset 6715:d9305abd02e9 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 6714:3b7f009f1a46 by rene thiemann _rene.thiemann@uibk.ac.at_:
improved bisection algorithm for algebraic numbers
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
Changeset 6713:e2a87698dd16 by rene thiemann _rene.thiemann@uibk.ac.at_:
added select_correct_factor_rat_poly as common factor+bisect algorithm
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Sturm_Rat.thy (diff)
Changeset 6712:25cbadea547f by rene thiemann _rene.thiemann@uibk.ac.at_:
soundness of select_correct_factor
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
Changeset 6711:16fbb05f2461 by Andreas Lochbihler:
use BNF_Corec in Stern_Brocot
The file was modified thys/Stern_Brocot/Bird_Tree.thy (diff)
The file was modified thys/Stern_Brocot/Cotree.thy (diff)
The file was modified thys/Stern_Brocot/Cotree_Algebra.thy (diff)
The file was modified thys/Stern_Brocot/ROOT (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)