equal
deleted
inserted
replaced
29 |
29 |
30 |
30 |
31 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
31 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
32 with result type T. The call creates a new term expecting one argument |
32 with result type T. The call creates a new term expecting one argument |
33 of type S.*) |
33 of type S.*) |
34 fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u = |
34 fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u = |
35 internal_split_const (T1, T2, T3) $ |
35 internal_split_const (T1, T2, T3) $ |
36 Abs ("v", T1, |
36 Abs ("v", T1, |
37 ap_split T2 T3 |
37 ap_split T2 T3 |
38 ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $ |
38 ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $ |
39 Bound 0)) |
39 Bound 0)) |