Skip to content
Success

Changes

Summary

  1. global interpretation into nested targets
  2. more succint interfaces
Changeset 73846:9447668d1b77 by haftmann:
global interpretation into nested targets
The file was addedsrc/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)
Changeset 73845:bfce186331be by haftmann:
more succint interfaces
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)