Summary
- merged
- added mbox-like latex sugar
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) |