--- a/NEWS Thu Oct 01 23:49:05 2009 +0200
+++ b/NEWS Fri Oct 02 00:10:08 2009 +0200
@@ -15,6 +15,14 @@
* On instantiation of classes, remaining undefined class parameters
are formally declared. INCOMPATIBILITY.
+* Locale interpretation propagates mixins along the locale hierarchy.
+The currently only available mixins are the equations used to map
+local definitions to terms of the target domain of an interpretation.
+
+* Reactivated diagnositc command 'print_interps'. Use 'print_interps l'
+to print all interpretations of locale l in the theory. Interpretations
+in proofs are not shown.
+
*** HOL ***
--- a/src/Pure/Isar/expression.ML Thu Oct 01 23:49:05 2009 +0200
+++ b/src/Pure/Isar/expression.ML Fri Oct 02 00:10:08 2009 +0200
@@ -820,7 +820,8 @@
#-> (fn eqns => fold (fn ((dep, morph), wits) =>
fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
(map (Element.morph_witness export') wits))
- (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
+ (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
+ export thy) (deps ~~ witss)));
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
--- a/src/Pure/Isar/locale.ML Thu Oct 01 23:49:05 2009 +0200
+++ b/src/Pure/Isar/locale.ML Fri Oct 02 00:10:08 2009 +0200
@@ -68,8 +68,10 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations and dependencies *)
- val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
- val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
+ val add_registration: string * morphism -> (morphism * bool) option ->
+ morphism -> theory -> theory
+ val amend_registration: string * morphism -> morphism * bool ->
+ morphism -> theory -> theory
val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
val add_dependency: string -> string * morphism -> morphism -> theory -> theory
@@ -474,7 +476,8 @@
|> roundup thy add_reg export (name, base_morph)
|> snd
(* add mixin *)
- |> amend_registration (name, base_morph) mixin export
+ |> (case mixin of NONE => I
+ | SOME mixin => amend_registration (name, base_morph) mixin export)
(* activate import hierarchy as far as not already active *)
|> Context.theory_map (activate_facts' export (name, base_morph))
end