Summary
- global interpretation into nested targets
- more succint interfaces
The file was added | src/HOL/ex/Interpretation_in_nested_targets.thy |
The file was modified | NEWS (diff) |
The file was modified | src/Doc/Isar_Ref/Spec.thy (diff) |
The file was modified | src/HOL/Library/Lexord.thy (diff) |
The file was modified | src/Pure/Isar/generic_target.ML (diff) |
The file was modified | src/Pure/Isar/local_theory.ML (diff) |
The file was modified | src/Pure/Isar/class.ML (diff) |
The file was modified | src/Pure/Isar/class_declaration.ML (diff) |
The file was modified | src/Pure/Isar/generic_target.ML (diff) |
The file was modified | src/Pure/Isar/interpretation.ML (diff) |
The file was modified | src/Pure/Isar/locale.ML (diff) |
The file was modified | src/Pure/Isar/named_target.ML (diff) |
The file was modified | src/Pure/Isar/overloading.ML (diff) |