equal
deleted
inserted
replaced
86 (*global.c xs == rhs'*) global_def, |
86 (*global.c xs == rhs'*) global_def, |
87 (*rhs' == rhs*) Thm.symmetric rhs_conv]; |
87 (*rhs' == rhs*) Thm.symmetric rhs_conv]; |
88 |
88 |
89 (*note*) |
89 (*note*) |
90 val ([(res_name, [res])], lthy4) = lthy3 |
90 val ([(res_name, [res])], lthy4) = lthy3 |
91 |> Local_Theory.notes_kind "" |
91 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; |
92 [((if internal then Binding.empty else b_def, atts), [([def], [])])]; |
|
93 in ((lhs, (res_name, res)), lthy4) end; |
92 in ((lhs, (res_name, res)), lthy4) end; |
94 |
93 |
95 |
94 |
96 (* notes *) |
95 (* notes *) |
97 |
96 |