Summary
- clarified signature: proper result;
- new theorem about exposed faces
The file was modified | src/HOL/Tools/Function/partial_function.ML (diff) |
The file was modified | src/HOL/Analysis/Polytope.thy (diff) |
The file was modified | src/HOL/Tools/Function/partial_function.ML (diff) |
The file was modified | src/HOL/Analysis/Polytope.thy (diff) |