equal
deleted
inserted
replaced
517 quotient_definition |
517 quotient_definition |
518 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
518 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
519 as "delete_raw" |
519 as "delete_raw" |
520 |
520 |
521 quotient_definition |
521 quotient_definition |
522 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50) |
|
523 as "op @" |
|
524 |
|
525 quotient_definition |
|
526 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
522 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
527 as "inter_raw" |
523 as "inter_raw" |
528 |
524 |
529 quotient_definition |
525 quotient_definition |
530 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
526 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |