Commit 34fe655b authored by Heiko Becker's avatar Heiko Becker

Tweak Daisy computelib in HOL4 to make checking great again

parent 4453f63d
......@@ -2,7 +2,9 @@ structure DaisyCompLib =
struct
open computeLib;
val _ = computeLib.add_funs [sptreeTheory.subspt_eq];
val _ = computeLib.del_funs [sptreeTheory.subspt_def];
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER];
val _ = computeLib.add_funs [sptreeTheory.subspt_eq];
end
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../ ../Infra ../cakeml/
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../ ../Infra ../cakeml/misc
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......
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