Lines Matching defs:guess
38 simple_guess_type -> (* which type of guess should be searched *)
39 term -> (* var to search a guess for *)
254 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
256 val thm0 = HO_MATCH_MP SIMPLE_GUESS_EXISTS_THM (GEN v guess)
275 val guess = combine_sgsfwcs wcl avoid sgty_forall v b_tm
277 val thm0 = HO_MATCH_MP SIMPLE_GUESS_FORALL_THM (GEN v guess)
289 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
291 val thm0 = HO_MATCH_MP SIMPLE_GUESS_UEXISTS_THM (GEN v guess)
302 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
304 val thm0 = HO_MATCH_MP SIMPLE_GUESS_SOME_THM (GEN v guess)
315 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
317 val thm0 = HO_MATCH_MP SIMPLE_GUESS_SELECT_THM (GEN v guess)