Commit 27105163 authored by Heiko Becker's avatar Heiko Becker

Add workaround tactic

parent c77e6a53
......@@ -102,11 +102,14 @@ 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
fun daisy_eval_tac t :tactic=
let
val result_thm = computeLib.EVAL_CONV t
in
rewrite_tac [result_thm]
\\ fs[sptreeTheory.lookup_def]
\\ rpt strip_tac
\\ fs[sptreeTheory.lookup_def]
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