equal
deleted
inserted
replaced
368 translations |
368 translations |
369 "{|x, xs|}" == "CONST finsert x {|xs|}" |
369 "{|x, xs|}" == "CONST finsert x {|xs|}" |
370 "{|x|}" == "CONST finsert x {||}" |
370 "{|x|}" == "CONST finsert x {||}" |
371 |
371 |
372 quotient_definition |
372 quotient_definition |
373 fin ("_ |\<in>| _" [50, 51] 50) |
373 fin (infix "|\<in>|" 50) |
374 where |
374 where |
375 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
375 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
376 |
376 |
377 abbreviation |
377 abbreviation |
378 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
378 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |