1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
#=================================================================
#
# MAKEFILE FOR THE HOL LIBRARY: more_arithmetic
#
# =====================================================================
# =====================================================================
# MAIN ENTRIES:
#
# make all : create theories
#
# make clean : remove only compiled code
#
# make clobber : remove both theories and compiled code
#
# ---------------------------------------------------------------------
#
# MACROS:
#
# Hol : the pathname of the version of hol used
# =====================================================================
Hol=../../hol
# =====================================================================
# Cleaning functions.
# =====================================================================
clean:
rm -f *_ml.o
@echo "===> library more_arithmetic: all object code deleted"
clobber:
rm -f *_ml.o *_ml.l *.th
@echo "===> library more_arithmetic: all object code and theory files deleted"
# =====================================================================
# Entries for individual files.
# =====================================================================
more_arithmetic.th: mk_more_arithmetic.ml pre.th sub.th mult.th odd_even.th min_max.th div_mod.th
rm -f more_arithmetic.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `mk_more_arithmetic`;;'\
'quit();;' | ${Hol}
ineq.th: ineq.ml
rm -f ineq.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `ineq`;;'\
'quit();;' | ${Hol}
zero_ineq.th: zero.ml ineq.th
rm -f zero_ineq.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `zero`;;'\
'quit();;' | ${Hol}
suc.th: suc.ml ineq.th
rm -f suc.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `suc`;;'\
'quit();;' | ${Hol}
add.th: add.ml suc.th
rm -f add.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `add`;;'\
'quit();;' | ${Hol}
pre.th: pre.ml ineq.th
rm -f pre.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `pre`;;'\
'quit();;' | ${Hol}
sub.th: sub.ml add.th zero_ineq.th
rm -f sub.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `sub`;;'\
'quit();;' | ${Hol}
mult.th: mult.ml ineq.th
rm -f mult.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `mult`;;'\
'quit();;' | ${Hol}
min_max.th: minmax.ml
rm -f min_max.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `minmax`;;'\
'quit();;' | ${Hol}
odd_even.th: odd_even.ml
rm -f odd_even.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `odd_even`;;'\
'quit();;' | ${Hol}
div_mod.th: div_mod.ml
rm -f div_mod.th
echo 'set_flag(`abort_when_fail`,true);;'\
'loadt `div_mod`;;'\
'quit();;' | ${Hol}
num_convs_ml.o: num_convs.ml more_arithmetic.th more_arithmetic.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'compilet `num_convs`;;'\
'quit();;' | ${Hol}
num_tac_ml.o: num_tac.ml more_arithmetic.th more_arithmetic.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'compilet `num_tac`;;'\
'quit();;' | ${Hol}
# =====================================================================
# Main entry
# =====================================================================
all: more_arithmetic.th num_convs_ml.o num_tac_ml.o
@echo "===> library more_arithmetic rebuilt"
|
