equal
deleted
inserted
replaced
14 |
14 |
15 val dest_listT: typ -> typ |
15 val dest_listT: typ -> typ |
16 val dest_fsetT: typ -> typ |
16 val dest_fsetT: typ -> typ |
17 |
17 |
18 val mk_id: term -> term |
18 val mk_id: term -> term |
|
19 val mk_all: (string * typ) -> term -> term |
19 |
20 |
20 val size_const: typ -> term |
21 val size_const: typ -> term |
21 |
22 |
22 val sum_case_const: typ -> typ -> typ -> term |
23 val sum_case_const: typ -> typ -> typ -> term |
23 val mk_sum_case: term -> term -> term |
24 val mk_sum_case: term -> term -> term |
151 let |
152 let |
152 val ty = fastype_of trm |
153 val ty = fastype_of trm |
153 in |
154 in |
154 Const (@{const_name id}, ty --> ty) $ trm |
155 Const (@{const_name id}, ty --> ty) $ trm |
155 end |
156 end |
|
157 |
|
158 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
156 |
159 |
157 |
160 |
158 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
161 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
159 |
162 |
160 fun sum_case_const ty1 ty2 ty3 = |
163 fun sum_case_const ty1 ty2 ty3 = |