equal
deleted
inserted
replaced
288 "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
288 "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
289 is "Cons" by auto |
289 is "Cons" by auto |
290 |
290 |
291 syntax |
291 syntax |
292 "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>) |
292 "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>) |
293 syntax_consts |
|
294 insert_fset |
|
295 translations |
293 translations |
296 "{|x, xs|}" == "CONST insert_fset x {|xs|}" |
294 "{|x, xs|}" == "CONST insert_fset x {|xs|}" |
297 "{|x|}" == "CONST insert_fset x {||}" |
295 "{|x|}" == "CONST insert_fset x {||}" |
298 |
296 |
299 quotient_definition |
297 quotient_definition |