601 quotient_definition

   601 quotient_definition

   602   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"

   602   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"

   603 is

   603 is

   604   "concat"

   604   "concat"

   605 

   605 

   606 quotient_definition

   608 quotient_definition

   607   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

   609   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

   608 is

   610 is

   609   "filter"

   611   "filter"

   610 

   612