136 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
136 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
137 [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}]) |
137 [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}]) |
138 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
138 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
139 [[typedef_thm, T_def] MRSL @{thm typedef_right_total}]) |
139 [[typedef_thm, T_def] MRSL @{thm typedef_right_total}]) |
140 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
140 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
|
141 [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}]) |
|
142 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
141 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}]) |
143 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}]) |
142 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
144 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
143 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}]) |
145 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}]) |
144 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
146 |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), |
145 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}]) |
147 [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}]) |