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

## Summary

- renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)

thys/Linear_Inequalities/Integer_Hull.thy | |

thys/Linear_Inequalities/Integral_Bounded_Vectors.thy | |

thys/Linear_Inequalities/Mixed_Integer_Solutions.thy |