Summary
- Back to original example theorem.
- Improved error reporting when activating a locale instance.
The file was modified | src/Doc/Locales/Examples.thy (diff) |
The file was modified | src/Doc/Locales/Examples3.thy (diff) |
The file was modified | src/Pure/Isar/locale.ML (diff) |