Skip to content
Success

Changes

Summary

  1. Back to original example theorem.
  2. Improved error reporting when activating a locale instance.
Changeset 63724:e7df93d4d9b8 by ballarin:
Back to original example theorem.
The file was modified src/Doc/Locales/Examples.thy (diff)
The file was modified src/Doc/Locales/Examples3.thy (diff)
Changeset 63723:dacc380ab327 by ballarin:
Improved error reporting when activating a locale instance.
The file was modified src/Pure/Isar/locale.ML (diff)