equal
deleted
inserted
replaced
286 |
286 |
287 quotient_definition |
287 quotient_definition |
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 nonterminal fset_args |
291 syntax |
292 syntax |
292 "_insert_fset" :: "args => 'a fset" ("{|(_)|}") |
293 "" :: "'a \<Rightarrow> fset_args" ("_") |
293 |
294 "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args" ("_,/ _") |
|
295 "_fset" :: "fset_args => 'a fset" ("{|(_)|}") |
294 syntax_consts |
296 syntax_consts |
295 "_insert_fset" == insert_fset |
297 "_fset_args" "_fset" == insert_fset |
296 |
|
297 translations |
298 translations |
298 "{|x, xs|}" == "CONST insert_fset x {|xs|}" |
299 "{|x, xs|}" == "CONST insert_fset x {|xs|}" |
299 "{|x|}" == "CONST insert_fset x {||}" |
300 "{|x|}" == "CONST insert_fset x {||}" |
300 |
301 |
301 quotient_definition |
302 quotient_definition |