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