136 |
136 |
137 (*instantiate class rep*) |
137 (*instantiate class rep*) |
138 val lthy = thy |
138 val lthy = thy |
139 |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain}) |
139 |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain}) |
140 val ((_, (_, emb_ldef)), lthy) = |
140 val ((_, (_, emb_ldef)), lthy) = |
141 Specification.definition NONE [] (emb_bind, emb_eqn) lthy |
141 Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy |
142 val ((_, (_, prj_ldef)), lthy) = |
142 val ((_, (_, prj_ldef)), lthy) = |
143 Specification.definition NONE [] (prj_bind, prj_eqn) lthy |
143 Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy |
144 val ((_, (_, defl_ldef)), lthy) = |
144 val ((_, (_, defl_ldef)), lthy) = |
145 Specification.definition NONE [] (defl_bind, defl_eqn) lthy |
145 Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy |
146 val ((_, (_, liftemb_ldef)), lthy) = |
146 val ((_, (_, liftemb_ldef)), lthy) = |
147 Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy |
147 Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy |
148 val ((_, (_, liftprj_ldef)), lthy) = |
148 val ((_, (_, liftprj_ldef)), lthy) = |
149 Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy |
149 Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy |
150 val ((_, (_, liftdefl_ldef)), lthy) = |
150 val ((_, (_, liftdefl_ldef)), lthy) = |
151 Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy |
151 Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy |
152 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) |
152 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) |
153 val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef |
153 val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef |
154 val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef |
154 val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef |
155 val defl_def = singleton (Proof_Context.export lthy ctxt_thy) defl_ldef |
155 val defl_def = singleton (Proof_Context.export lthy ctxt_thy) defl_ldef |
156 val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef |
156 val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef |