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 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
149 val lthy3 = quotdata_update (Binding.str_of qty_name) |
|
150 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
150 |
151 |
151 (* interpretation *) |
152 (* interpretation *) |
152 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
153 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
153 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
154 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
154 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
155 val eqn1i = Thm.prop_of (symmetric eqn1pre) |