Summary
- merged
- added eta_expansion and its documentation.
The file was modified | src/Doc/Sugar/Sugar.thy (diff) |
The file was modified | src/HOL/Library/LaTeXsugar.thy (diff) |
The file was modified | src/Doc/Sugar/Sugar.thy (diff) |
The file was modified | src/HOL/Library/LaTeXsugar.thy (diff) |