equal
deleted
inserted
replaced
38 where "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))" |
38 where "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))" |
39 |
39 |
40 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" |
40 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" |
41 where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
41 where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
42 |
42 |
43 syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))") |
43 nonterminal stuple_args |
44 syntax_consts "_stuple" \<rightleftharpoons> spair |
44 syntax |
|
45 "" :: "logic \<Rightarrow> stuple_args" ("_") |
|
46 "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args" ("_,/ _") |
|
47 "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic" ("(1'(:_,/ _:'))") |
|
48 syntax_consts |
|
49 "_stuple_args" "_stuple" \<rightleftharpoons> spair |
45 translations |
50 translations |
46 "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)" |
51 "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)" |
47 "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y" |
52 "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y" |
48 |
53 |
49 translations |
54 translations |