# ieee Makefile

CONTEXT = ieee
FILES = \
add_zero.pvs \
alpha_equiv.pvs \
alpha_sticky.pvs \
compare.pvs \
bv2fact.pvs     \
enum.pvs        \
except.pvs      \
factoring.pvs   \
fpop_result.pvs \
ieee_import.pvs \
inx.pvs         \
nu_format.pvs   \
rd2int.pvs      \
round.pvs       \
round_fact.pvs \
round_props.pvs \
sigrd.pvs       \
wrapped_exp.pvs

all: $(CONTEXT).pvs # prove.el

$(CONTEXT).pvs: $(FILES)
	../theories.pl $(CONTEXT) $(FILES) > $@

prove.el: $(FILES)
	../prove.pl $(FILES) > $@