Skip to content
Success

Changes

Summary

  1. merged
  2. Simplified some proofs
  3. added lemmas; internalized defn in class
Changeset 72386:6846b6df9a5f by paulson:
merged
Changeset 72385:4a2c0eb482aa by paulson _lp15@cam.ac.uk_:
Simplified some proofs
The file was modified src/HOL/Analysis/Convex.thy (diff)
Changeset 72384:b037517c815b by nipkow:
added lemmas; internalized defn in class
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)