Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merge
  2. compute |lc(f)| * factor_bound f instead of factor_bound (lc(f) * f)
Changeset 7456:ce14515f35d6 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 7455:105f9d4a963e by rene thiemann _rene.thiemann@uibk.ac.at_:
compute |lc(f)| * factor_bound f instead of factor_bound (lc(f) * f)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Zassenhaus.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Factor_Bound.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Reconstruction.thy (diff)