changeset 794 | f0a78fda343f |
parent 793 | 09dff5ef8f74 |
child 796 | 64f9c76f70c7 |
--- a/Quot/Examples/FSet3.thy Sat Dec 26 20:24:53 2009 +0100 +++ b/Quot/Examples/FSet3.thy Sat Dec 26 20:45:37 2009 +0100 @@ -519,10 +519,6 @@ as "delete_raw" quotient_definition - "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50) - as "op @" - -quotient_definition "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) as "inter_raw"