changeset 81091 | c007e6d9941d |
parent 81089 | 8042869c2072 |
child 81095 | 49c04500c5f9 |
--- a/src/HOL/HOLCF/LowerPD.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/LowerPD.thy Tue Oct 01 20:39:16 2024 +0200 @@ -135,8 +135,6 @@ syntax "_lower_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix lower_pd enumeration\<close>\<close>{_}\<flat>)\<close>) -syntax_consts - lower_add translations "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>" "{x}\<flat>" == "CONST lower_unit\<cdot>x"