equal
deleted
inserted
replaced
19 struct |
19 struct |
20 |
20 |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
21 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
22 |
22 |
23 (* @chunk definitions_aux *) |
23 (* @chunk definitions_aux *) |
24 fun definitions_aux s ((binding, syn), (attr, trm)) lthy = |
24 fun definitions_aux ((binding, syn), trm) lthy = |
25 let |
25 let |
26 val ((_, (_, thm)), lthy) = |
26 val ((_, (_, thm)), lthy) = |
27 LocalTheory.define s ((binding, syn), (attr, trm)) lthy |
27 LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy |
28 in |
28 in |
29 (thm, lthy) |
29 (thm, lthy) |
30 end |
30 end |
31 (* @end *) |
31 (* @end *) |
32 |
32 |
43 val t0 = list_comb (pred, zs); |
43 val t0 = list_comb (pred, zs); |
44 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
44 val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; |
45 val t2 = fold_rev mk_all preds' t1; |
45 val t2 = fold_rev mk_all preds' t1; |
46 val t3 = fold_rev lambda (params @ zs) t2; |
46 val t3 = fold_rev lambda (params @ zs) t2; |
47 in |
47 in |
48 definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3)) |
48 definitions_aux ((R, syn), t3) |
49 end) (preds ~~ preds' ~~ Tss) lthy |
49 end) (preds ~~ preds' ~~ Tss) lthy |
50 end |
50 end |
51 (* @end *) |
51 (* @end *) |
52 |
52 |
53 fun inst_spec ct = |
53 fun inst_spec ct = |