Skip to content
Success

Changes

Summary

  1. Another sum_nonneg fix for eba08da54c6b
  2. fixes for eba08da54c6b, especially sum_nonneg
  3. corrected for new sum_nonneg in eba08da54c6b
Changeset 7897:5e2ea58aa692 by paulson _lp15@cam.ac.uk_:
Another sum_nonneg fix for eba08da54c6b
The file was modified thys/Integration/Integral.thy (diff)
Changeset 7896:dc5564d8dd9d by paulson _lp15@cam.ac.uk_:
fixes for eba08da54c6b, especially sum_nonneg
The file was modified thys/Coinductive/Examples/LList_CCPO_Topology.thy (diff)
The file was modified thys/Markov_Models/ex/Crowds_Protocol.thy (diff)
The file was modified thys/pGCL/Healthiness.thy (diff)
Changeset 7895:3a01f27746e5 by paulson _lp15@cam.ac.uk_:
corrected for new sum_nonneg in eba08da54c6b
The file was modified thys/Cauchy/CauchySchwarz.thy (diff)