Lines Matching defs:goal
13 val goal = ``?a:'c b:'d. Q a b``
14 val (sgs, vfn) = Q.REFINE_EXISTS_TAC `f x y` ([asm], goal)
23 val _ = if aconv (concl result) goal then
52 aconvdie "goal" c expected_c0;
84 val _ = aconvdie "goal conclusion" c expected_mat1c
88 | _ => die "FAILED! (new goal of wrong shape)"
99 val _ = aconvdie "goal conclusion" c expected_mat2c
105 | _ => die "FAILED! (new goal of wrong shape)"
114 [([], t)] => (aconvdie "goal" t expected_result1; OK())
127 aconvdie "goal" t expected_result1;
138 (aconvdie "goal conclusion" t expected_result2; OK())
147 (aconvdie "goal conclusion" t expected_result2a; OK())
161 aconvdie "goal conclusion" c expected_c;
178 aconvdie "goal conclusion" c expected_c;