equal
deleted
inserted
replaced
141 where "{} \<equiv> bot" |
141 where "{} \<equiv> bot" |
142 |
142 |
143 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" |
143 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" |
144 where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}" |
144 where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}" |
145 |
145 |
|
146 nonterminal finset_args |
146 syntax |
147 syntax |
147 "_Finset" :: "args \<Rightarrow> 'a set" ("{(_)}") |
148 "" :: "'a \<Rightarrow> finset_args" ("_") |
|
149 "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args" ("_,/ _") |
|
150 "_Finset" :: "finset_args \<Rightarrow> 'a set" ("{(_)}") |
148 syntax_consts |
151 syntax_consts |
149 "_Finset" \<rightleftharpoons> insert |
152 "_Finset_args" "_Finset" \<rightleftharpoons> insert |
150 translations |
153 translations |
151 "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}" |
154 "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}" |
152 "{x}" \<rightleftharpoons> "CONST insert x {}" |
155 "{x}" \<rightleftharpoons> "CONST insert x {}" |
153 |
156 |
154 |
157 |