Lines Matching refs:list
8 val combinator_thmL : thm list
10 val final_decision_procedure : thm list -> term -> thm;
12 val resource_proccall_free_thmL : thm list
13 val inital_prop_rewrite_thmL : thm list
14 val abstrL : separationLogicLib.asl_program_abstraction list
15 val comments_step_convL : (conv->conv) list
16 val quantifier_heuristicsL : quantHeuristicsLib.quant_param list
18 (term list -> int -> (bool * simpLib.ssfrag) -> thm list -> term * term * term * term -> thm list) list
20 val hoare_triple_case_splitL : (term -> term) list
21 val frame_split_case_splitL : (term -> term) list
35 val COND_REWRITE_CONV : bool -> Abbrev.thm list -> Abbrev.conv
36 val GUARDED_COND_REWRITE_CONV : bool -> (Abbrev.term -> bool) -> Abbrev.thm list -> Abbrev.conv
44 val VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm
46 val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm
49 val VAR_RES_PROP_REWRITE_CONV : (bool * simpLib.ssfrag) -> thm list -> term -> thm
52 val VAR_RES_COND_HOARE_TRIPLE___RESORT_PRECOND_CONV : int list -> conv
53 val var_res_prop___COND_RESORT_CONV : int list -> conv
55 val cond_rewrite___varlist_update : thm list -> conv
56 val GENERATE___var_res_exp_varlist_update___REWRITES : term -> term -> term -> (term * thm list)
73 type var_res_inference = var_res_inference_param -> thm list -> ConseqConv.directed_conseq_conv
77 val context_strengthen_conseq_conv : (thm list -> conv) -> var_res_inference;
78 val simpset_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference;
80 val expands_strengthen_conseq_conv : (int -> (bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference;
83 val INFERENCES_LIST___simulate_command : (string * var_res_base.var_res_inference) list
84 val INFERENCES_LIST___simulate_minor_command : (string * var_res_base.var_res_inference) list
85 val INFERENCES_LIST___expensive_simplifications : (string * var_res_base.var_res_inference) list
86 val INFERENCES_LIST___entailment_steps : (string * var_res_base.var_res_inference) list
88 val VAR_RES_IS_PURE_PROPOSITION___provers : (term -> term -> thm) list
103 (string * holfoot_param.var_res_base.var_res_inference) list;
105 type user_rewrite_param = (Abbrev.thm list * Abbrev.conv list * simpLib.ssfrag list);
111 stop_evals : (Abbrev.term -> bool) list,
113 inferences : (int * var_res_inference_group) list *
114 (int * var_res_inference_group) list *
115 (int * var_res_inference_group) list};
124 | add_rewrites of Abbrev.thm list
125 | add_convs of Abbrev.conv list
126 | add_ssfrags of simpLib.ssfrag list
127 | stop_evals of (Abbrev.term -> bool) list
128 | combined_gen_step_tac_opt of gen_step_tac_opt list
129 | add_inference_groups of (int * var_res_inference_group) list *
130 (int * var_res_inference_group) list *
131 (int * var_res_inference_group) list;
160 val gen_step_param___update_stop_evals : gen_step_param -> (Abbrev.term -> bool) list -> gen_step_param
162 (int * var_res_inference_group) list *
163 (int * var_res_inference_group) list *
164 (int * var_res_inference_group) list) -> gen_step_param
167 (int * var_res_inference_group) list *
168 (int * var_res_inference_group) list *
169 (int * var_res_inference_group) list) -> gen_step_param
171 val VAR_RES_GEN_STEP_CONSEQ_CONV : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv
173 val xVAR_RES_GEN_STEP_CONSEQ_CONV: gen_step_tac_opt list -> int option -> int -> Abbrev.conv
174 val xVAR_RES_GEN_STEP_TAC : gen_step_tac_opt list -> int option -> int -> Abbrev.tactic
186 val add_rewrites : Abbrev.thm list -> holfoot_tactics.gen_step_tac_opt;
187 val add_convs : Abbrev.conv list -> holfoot_tactics.gen_step_tac_opt;
188 val add_ssfrags : simpLib.ssfrag list -> holfoot_tactics.gen_step_tac_opt;
189 val combined_gen_step_tac_opt : holfoot_tactics.gen_step_tac_opt list -> holfoot_tactics.gen_step_tac_opt;
190 val add_inference_groups : (int * holfoot_tactics.var_res_inference_group) list *
191 (int * holfoot_tactics.var_res_inference_group) list *
192 (int * holfoot_tactics.var_res_inference_group) list -> holfoot_tactics.gen_step_tac_opt
214 val default_holfoot_gst_optL : holfoot_tactics.gen_step_tac_opt list ref;
216 val HF_GEN_STEP_CONSEQ_CONV : holfoot_tactics.gen_step_param -> holfoot_tactics.user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv
218 val xHF_GEN_STEP_CONSEQ_CONV: holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.conv
219 val xHF_GEN_STEP_TAC : holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.tactic
221 val xHF_STEP_TAC : holfoot_tactics.gen_step_tac_opt list -> int -> Abbrev.tactic;
222 val xHF_STEP_TAC_n : holfoot_tactics.gen_step_tac_opt list -> int -> int option -> Abbrev.tactic;
223 val xHF_SOLVE_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
224 val xHF_CONTINUE_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
225 val xHF_SIMPLIFY_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic;
244 val holfoot_set_goal_specs : string -> string list -> proofManagerLib.proofs
245 val holfoot_set_goal_procedures : string -> string list -> proofManagerLib.proofs
247 val holfoot_verify_spec : string -> holfoot_tactics.gen_step_tac_opt list -> thm
248 val holfoot_tac_verify_spec : string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> thm
249 val holfoot_interactive_verify_spec : bool -> bool -> string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> (thm * bool)
253 val holfoot_prover_extras_1 : thm list ref;
254 val holfoot_prover_extras_2 : thm list ref;
255 val holfoot_varlist_rwts : thm list ref;