equal
deleted
inserted
replaced
1508 (strs2str o (map (linefeed o pair2str o |
1508 (strs2str o (map (linefeed o pair2str o |
1509 (apsnd term2str) o |
1509 (apsnd term2str) o |
1510 (apfst bool2str)))) bts; |
1510 (apfst bool2str)))) bts; |
1511 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) = |
1511 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) = |
1512 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^ |
1512 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^ |
1513 ", "^itms2str_ (thy2ctxt "Isac") itms^ |
1513 ", "^itms2str_ (thy2ctxt' "Isac") itms^ |
1514 ", "^preconds2str prec^", \n"^spec2str spec^" )"; |
1514 ", "^preconds2str prec^", \n"^spec2str spec^" )"; |
1515 |
1515 |
1516 |
1516 |
1517 |
1517 |
1518 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj; |
1518 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj; |