Summary
- Merge
- numerous theorems about affine hulls, hyperplanes, etc.
- merged
- proper LaTeX;
- tuned;
- clarified bindings;
- clarified bindings;
- tuned;
- tuned;
- avoid clash with function called "x";
The file was modified | src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Path_Connected.thy (diff) |
The file was modified | src/HOL/ex/Functions.thy (diff) |
The file was modified | src/HOL/Eisbach/Examples.thy (diff) |
The file was modified | src/HOL/Tools/Function/mutual.ML (diff) |
The file was modified | src/HOL/Tools/Function/function.ML (diff) |
The file was modified | src/HOL/Tools/Function/function_core.ML (diff) |
The file was modified | src/HOL/Tools/Function/function_lib.ML (diff) |
The file was modified | src/HOL/Tools/Function/mutual.ML (diff) |
The file was modified | src/HOL/Tools/Function/function_common.ML (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_def.ML (diff) |
The file was modified | src/HOL/Tools/Function/partial_function.ML (diff) |