src/translations/translationsLib.sml

274             val ds = dsExtractFromThm dsThm;
275             val thm = TSPECL [ds, hd args]
286             val ds = dsExtractFromThm dsThm;
290             val thm = SPECL [ds, hd args, pf] thm
300             val ds = dsExtractFromThm dsThm;
301             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
314             val ds = dsExtractFromThm dsThm;
315             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
328             val ds = dsExtractFromThm dsThm;
329             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
345             val ds = dsExtractFromThm dsThm;
346             val thm = TSPECL [ds, (boolToHOL b11), (boolToHOL b12), (boolToHOL b21), (boolToHOL b22), l1, l2, pf1, pf2]
360             val ds = dsExtractFromThm dsThm;
361             val thm = TSPECL [ds, (boolToHOL b11), (boolToHOL b12), (boolToHOL b21), (boolToHOL b22), l1, l2, pf1, pf2]
375             val ds = dsExtractFromThm dsThm;
376             val thm = TSPECL [ds, l1, l2, pf1, pf2]
390             val ds = dsExtractFromThm dsThm;
394             val thm = SPECL [ds, l1, l2, pf1, pf2] thm;
409             val ds = dsExtractFromThm dsThm;
413             val thm = SPECL [ds, l1, l2, pf1, pf2] thm;
428             val ds = dsExtractFromThm dsThm;
432             val thm = SPECL [ds, l1, l2, pf1, pf2] thm;
447             val ds = dsExtractFromThm dsThm;
449               (boolToHOL b22), ds, l1, l2, pf1, pf2]
475       val ds = dsExtractFromThm dsThm;
476       val set = el 6 (snd (strip_comb ds));
481       (ds, l, b1, b2, pf)
514             val (ds, l, _, _, pf) = dsSingBindingExtractFromThm dsThm;
515             val thm = TSPECL [boolToHOL b1, boolToHOL b2, ds, l, pf]  thm;
645       val ds = dsExtractFromThm thm;
649       (l, equivTHM, thm, ds, pf, b1', b2')
659         val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast b1 b2 l;
665         val thm = SPECL [ds, l, equivL, pf, boolToHOL a] thm;
710       val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast true false l;
714       val thm = SPECL [ds, l, equivL, pf, boolToHOL b2'] thm;
753       val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast false true l;
757       val thm = SPECL [ds, l, equivL, pf, boolToHOL b1'] thm;