Summary
- correction of TeX errors and other oversights
- Oops! Change_Of_Vars was not being imported to Analysis!
The file was modified | src/HOL/Analysis/Change_Of_Vars.thy (diff) |
The file was modified | src/HOL/Analysis/Analysis.thy (diff) |
The file was modified | src/HOL/Analysis/Change_Of_Vars.thy (diff) |
The file was modified | src/HOL/Analysis/Analysis.thy (diff) |