equal
deleted
inserted
replaced
4 Abstract syntax operations for HOL. |
4 Abstract syntax operations for HOL. |
5 *) |
5 *) |
6 |
6 |
7 signature HOLOGIC = |
7 signature HOLOGIC = |
8 sig |
8 sig |
9 val typeS: sort |
|
10 val typeT: typ |
|
11 val id_const: typ -> term |
9 val id_const: typ -> term |
12 val mk_comp: term * term -> term |
10 val mk_comp: term * term -> term |
13 val boolN: string |
11 val boolN: string |
14 val boolT: typ |
12 val boolT: typ |
15 val Trueprop: term |
13 val Trueprop: term |
139 end; |
137 end; |
140 |
138 |
141 structure HOLogic: HOLOGIC = |
139 structure HOLogic: HOLOGIC = |
142 struct |
140 struct |
143 |
141 |
144 (* HOL syntax *) |
|
145 |
|
146 val typeS: sort = ["HOL.type"]; |
|
147 val typeT = Type_Infer.anyT typeS; |
|
148 |
|
149 |
|
150 (* functions *) |
142 (* functions *) |
151 |
143 |
152 fun id_const T = Const ("Fun.id", T --> T); |
144 fun id_const T = Const ("Fun.id", T --> T); |
153 |
145 |
154 fun mk_comp (f, g) = |
146 fun mk_comp (f, g) = |