Commit 2804179b authored by Heiko Becker's avatar Heiko Becker

Add Daisy eval tactic

parent 4884374c
......@@ -102,4 +102,11 @@ fun impl_subgoal_tac th =
SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
end
val daisy_eval_tac :tactic=
let
val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, sptreeTheory.subspt_eq]
in EVAL_TAC
end;
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment