equal
deleted
inserted
replaced
368 |
368 |
369 fun theory_declaration decl = |
369 fun theory_declaration decl = |
370 background_declaration decl #> standard_declaration (K true) decl; |
370 background_declaration decl #> standard_declaration (K true) decl; |
371 |
371 |
372 val theory_registration = |
372 val theory_registration = |
373 Local_Theory.raw_theory o Context.theory_map o Locale.add_registration; |
373 Local_Theory.raw_theory o Locale.add_registration_theory; |
374 |
374 |
375 |
375 |
376 |
376 |
377 (** locale target primitives **) |
377 (** locale target primitives **) |
378 |
378 |