1signature ibmLib = 2sig 3 4val ibm_to_ks : Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm 5val ibm_to_ks_total : Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm -> 6Abbrev.thm 7val ibm_to_ks_total_cheat : Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm 8 9val ibm_to_ks_clock_total : Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm -> 10Abbrev.thm 11val ibm_to_ks_clock_total_cheat : Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm 12 13val make_total_thm : Abbrev.term -> Abbrev.thm 14val model_check_ibm : bool -> Abbrev.term -> Abbrev.term -> Abbrev.term -> Abbrev.thm option 15 16 17end 18 19