Summary
- merged
- Simplified some proofs
- added lemmas; internalized defn in class
The file was modified | src/HOL/Analysis/Convex.thy (diff) |
The file was modified | src/HOL/Finite_Set.thy (diff) |
The file was modified | src/HOL/Lattices_Big.thy (diff) |
The file was modified | src/HOL/Analysis/Convex.thy (diff) |
The file was modified | src/HOL/Finite_Set.thy (diff) |
The file was modified | src/HOL/Lattices_Big.thy (diff) |