Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. document change in metadata
  2. generalized fixed bounds on determinants to predicate; added an improved determinate bound -> result: get smaller bound on mixed integer solutions (replace n! by sqrt(n^n))
Changeset 12768:6927929601ba by rene thiemann _rene.thiemann@uibk.ac.at_:
document change in metadata
The file was modified metadata/entries/Linear_Inequalities.toml
Changeset 12767:6cf62d8e618e by rene thiemann _rene.thiemann@uibk.ac.at_:
generalized fixed bounds on determinants to predicate; added an improved determinate bound<br>-&gt; result: get smaller bound on mixed integer solutions&nbsp; (replace n! by sqrt(n^n))
The file was modified thys/Linear_Inequalities/Decomposition_Theorem.thy
The file was modified thys/Linear_Inequalities/Farkas_Minkowsky_Weyl.thy
The file was modified thys/Linear_Inequalities/Integer_Hull.thy
The file was modified thys/Linear_Inequalities/Integral_Bounded_Vectors.thy
The file was modified thys/Linear_Inequalities/Mixed_Integer_Solutions.thy
The file was modified thys/Linear_Inequalities/Normal_Vector.thy
The file was modified thys/Linear_Inequalities/document/root.tex