Lines Matching defs:guess
34 datatype guess =
39 val is_guess_general : guess -> bool
40 val is_guess_thm : guess_type -> guess -> bool
41 val is_guess_term : guess_type -> guess -> bool
42 val is_guess : guess_type -> guess -> bool
43 val guess_has_thm : guess -> bool
44 val guess_has_no_free_vars : guess -> bool
45 val guess_has_thm_no_free_vars : guess -> bool
51 val guess_remove_thm : term -> term -> guess -> guess
52 val make_set_guess_thm : guess -> (term -> thm) -> guess
53 val mk_guess : guess_type -> term -> term -> term -> term list -> guess
54 val mk_guess_opt : guess_type option -> term -> term -> term -> term list -> guess
56 val make_guess___dummy : guess_type -> term -> term -> term -> term list -> guess
57 val make_guess___assume : guess_type -> term -> term -> term -> term list -> guess
58 val make_guess___simple : guess_type -> term -> term -> term -> term list -> guess
60 val make_set_guess_thm___dummy : guess -> guess
61 val make_set_guess_thm___simple : guess -> guess
62 val make_set_guess_thm___assume : guess -> guess
64 val guess_extract : guess -> term * term list
65 val guess_extract_thm : guess -> guess_type * term * term list * thm * bool
66 val guess2term : guess -> term option
67 val guess2thm : guess -> bool * thm
68 val guess2thm_opt : guess -> thm option
69 val guess_extract_type : guess -> guess_type option
72 val guess_thm_to_guess : bool -> (term * term list) option -> thm -> guess
76 val guess_to_string : bool -> guess -> string
84 general : guess list,
85 exists_point : guess list,
86 forall_point : guess list,
87 forall : guess list,
88 exists : guess list,
89 forall_gap : guess list,
90 exists_gap : guess list}
92 val guess_collection_guess_type : guess_type -> guess_collection -> guess list
98 val guess_list2collection : thm list * guess list -> guess_collection;
99 val guess_collection2list : guess_collection -> thm list * guess list;
100 val guess_collection___get_exists_weaken : guess_collection -> guess list;
101 val guess_collection___get_forall_weaken : guess_collection -> guess list;
105 val guess_weaken : guess -> guess
106 val check_guess : term -> term -> guess -> bool
107 val correct_guess : term -> term -> guess -> guess option
108 val correct_guess_list : term -> term -> guess list -> guess list;