144 (* quotient theorem *) |
144 (* quotient theorem *) |
145 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
145 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
146 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
146 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
147 |
147 |
148 (* storing the quot-info *) |
148 (* storing the quot-info *) |
149 val lthy3 = quotdata_update (Binding.str_of qty_name) |
149 val qty_str = fst (dest_Type abs_ty) |
|
150 val lthy3 = quotdata_update qty_str |
150 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
151 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
151 |
152 |
152 (* interpretation *) |
153 (* interpretation *) |
153 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
154 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
154 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
155 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |