1signature modelTools =
2sig
3    include Abbrev
4
5type term_bdd = PrimitiveBddRules.term_bdd
6type model
7type ic = internalCacheTools.ic
8
9val empty_model : model
10
11val get_init : model -> Term.term
12val get_trans : model ->(string * Term.term) list
13val get_flag_ric : model -> bool
14val get_name : model -> string option
15val get_vord : model -> string list option
16val get_state : model -> Term.term option
17val get_props : model ->  (string * Term.term) list
18val get_results : model -> (PrimitiveBddRules.term_bdd * Thm.thm option * Term.term list option) list option
19val get_ic : model -> ic option
20val get_flag_abs : model -> bool
21
22val set_init : Term.term -> model -> model
23val set_trans : (string * Term.term) list -> model -> model
24val set_flag_ric : bool -> model -> model
25val set_name : string -> model -> model
26val set_vord : string list -> model -> model
27val set_state : Term.term -> model -> model
28val set_props :  (string * Term.term) list -> model -> model
29val set_results : (PrimitiveBddRules.term_bdd * Thm.thm option * Term.term list option) list -> model -> model
30val set_ic : ic -> model -> model
31val set_flag_abs : bool -> model -> model
32
33
34val dest_model :
35    model -> Term.term * (string * Term.term) list * bool * string option * string list option
36    * Term.term option * (string * Term.term) list
37    * (PrimitiveBddRules.term_bdd * Thm.thm option * Term.term list option) list option
38    * ic option
39
40val prove_model : model -> model
41
42end
43