102 notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), |
102 notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), |
103 abbrev = Generic_Target.locale_abbrev locale, |
103 abbrev = Generic_Target.locale_abbrev locale, |
104 declaration = Generic_Target.locale_declaration locale, |
104 declaration = Generic_Target.locale_declaration locale, |
105 theory_registration = fn _ => error "Not possible in locale target", |
105 theory_registration = fn _ => error "Not possible in locale target", |
106 locale_dependency = Generic_Target.locale_dependency locale, |
106 locale_dependency = Generic_Target.locale_dependency locale, |
107 pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale} |
107 pretty = fn ctxt => |
|
108 [Pretty.block (Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale)]} |
108 | operations (Class class) = |
109 | operations (Class class) = |
109 {define = Generic_Target.define (class_foundation class), |
110 {define = Generic_Target.define (class_foundation class), |
110 notes = Generic_Target.notes (Generic_Target.locale_target_notes class), |
111 notes = Generic_Target.notes (Generic_Target.locale_target_notes class), |
111 abbrev = Class.abbrev class, |
112 abbrev = Class.abbrev class, |
112 declaration = Generic_Target.locale_declaration class, |
113 declaration = Generic_Target.locale_declaration class, |