QuotMain.thy
changeset 354 2eb6d527dfe4
parent 353 9a0e8ab42ee8
child 355 abc6bfd0576e
equal deleted inserted replaced
353:9a0e8ab42ee8 354:2eb6d527dfe4
  1372 *}
  1372 *}
  1373 
  1373 
  1374 (* rep-abs injection *)
  1374 (* rep-abs injection *)
  1375 
  1375 
  1376 ML {*
  1376 ML {*
  1377 (* FIXME: is this the right get_fun function for rep-abs injection *)
       
  1378 fun mk_repabs lthy (T, T') trm = 
  1377 fun mk_repabs lthy (T, T') trm = 
  1379   Quotient_Def.get_fun repF lthy (T, T') 
  1378   Quotient_Def.get_fun repF lthy (T, T') 
  1380   $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
  1379     $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
  1381 *}
  1380 *}
  1382 
  1381 
  1383 ML {* length *}
       
  1384 
  1382 
  1385 ML {*
  1383 ML {*
  1386 (* bound variables need to be treated properly,  *)
  1384 (* bound variables need to be treated properly,  *)
  1387 (* as the type of subterms need to be calculated *)
  1385 (* as the type of subterms need to be calculated *)
  1388 
  1386