Summary
- take qualification of type name more seriously: derived consts and facts are qualified uniformly;
The file was modified | src/HOL/Import/import_rule.ML (diff) |
The file was modified | src/HOL/Tools/hologic.ML (diff) |
The file was modified | src/HOL/Tools/typedef.ML (diff) |