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