| changeset 81182 | fc5066122e68 |
| parent 81095 | 49c04500c5f9 |
| child 81583 | b6df83045178 |
--- a/src/HOL/HOLCF/Sprod.thy Fri Oct 18 11:44:05 2024 +0200 +++ b/src/HOL/HOLCF/Sprod.thy Fri Oct 18 14:20:09 2024 +0200 @@ -42,6 +42,8 @@ syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>) +syntax_consts + "_stuple" \<rightleftharpoons> spair translations "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)" "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"