equal
deleted
inserted
replaced
113 @ relator_distr bnf |
113 @ relator_distr bnf |
114 in |
114 in |
115 snd (Local_Theory.notes notes lthy) |
115 snd (Local_Theory.notes notes lthy) |
116 end |
116 end |
117 |
117 |
118 val _ = Context.>> (Context.map_theory (bnf_interpretation |
118 val _ = Theory.setup (bnf_interpretation |
119 (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation)) |
119 (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation)) |
120 (bnf_only_type_ctr lifting_bnf_interpretation))) |
120 (bnf_only_type_ctr lifting_bnf_interpretation)) |
121 |
121 |
122 end |
122 end |