changeset 81091 | c007e6d9941d |
parent 81019 | dd59daa3c37a |
child 81095 | 49c04500c5f9 |
--- a/src/HOL/HOLCF/Sprod.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 01 20:39:16 2024 +0200 @@ -42,8 +42,6 @@ syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>) -syntax_consts - spair translations "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)" "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"