Summary
- more accurate export morphism enables proper instantiation by interpretation
The file was modified | src/HOL/Library/Saturated.thy (diff) |
The file was modified | src/Pure/Isar/class.ML (diff) |
The file was modified | src/HOL/Library/Saturated.thy (diff) |
The file was modified | src/Pure/Isar/class.ML (diff) |