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 qty_str = fst (dest_Type abs_ty) |
149 val qty_str = fst (Term.dest_Type abs_ty) |
150 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
150 val _ = tracing ("storing under: " ^ qty_str) |
|
151 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
151 (* FIXME: varifyT should not be used *) |
152 (* FIXME: varifyT should not be used *) |
152 (* the type name maybe should be calculated via qty_name and Sign.intern_type *) |
|
153 |
153 |
154 (* interpretation *) |
154 (* interpretation *) |
155 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
155 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
156 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
156 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
157 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
157 val eqn1i = Thm.prop_of (symmetric eqn1pre) |