Changes

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

Summary

  1. renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)
Changeset 12770:365c3d8497ce by rene thiemann _rene.thiemann@uibk.ac.at_:
renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)
The file was modifiedthys/Linear_Inequalities/Integer_Hull.thy
The file was modifiedthys/Linear_Inequalities/Integral_Bounded_Vectors.thy
The file was modifiedthys/Linear_Inequalities/Mixed_Integer_Solutions.thy