Lines Matching defs:model
6 type model = modelTools.model
8 val holCheck : model -> model
12 val empty_model : model
14 val set_init : Term.term -> model -> model
15 val set_trans : (string * Term.term) list -> model -> model
16 val set_flag_ric : bool -> model -> model
17 val set_name : string -> model -> model
18 val set_vord : string list -> model -> model
19 val set_state : Term.term -> model -> model
20 val set_props : (string * Term.term) list -> model -> model
21 val set_flag_abs : bool -> model -> model
23 val get_init : model -> Term.term
24 val get_trans : model -> (string * Term.term) list
25 val get_flag_ric : model -> bool
26 val get_name : model -> string option
27 val get_vord : model -> string list option
28 val get_state : model -> Term.term option
29 val get_props : model -> (string * Term.term) list
30 val get_results : model -> (term_bdd * Thm.thm option * Term.term list option) list option
31 val get_flag_abs : model -> bool
33 val prove_model : model -> model