Lines Matching defs:goal
26 fun mk_Z3_fun name pre cmd_stem post goal =
29 SolverSpec.make_solver pre (file ^ cmd_stem) post goal
37 (fn goal =>
39 val (goal, _) = SolverSpec.simplify (SmtLib.SIMP_TAC false) goal
40 val (_, strings) = SmtLib.goal_to_SmtLib goal
77 (fn goal =>
79 val (goal, validation) = SolverSpec.simplify (SmtLib.SIMP_TAC true) goal
80 val (ty_tm_dict, strings) = SmtLib.goal_to_SmtLib_with_get_proof goal
82 (((goal, validation), ty_tm_dict), strings)
85 (fn ((goal, validation), (ty_dict, tm_dict)) =>
120 val (As, g) = goal