# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271834035 -7200
# Node ID 880fe1d2234e9e2fe2d264b23ba216a99b88c1f3
# Parent  7b74cf8439422062007a0caf4286ebf172db4b46# Parent  0dc61c2966da484e85ea8ab01363df5b083ea230
merge

diff -r 0dc61c2966da -r 880fe1d2234e Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Apr 20 17:25:31 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 09:13:55 2010 +0200
@@ -563,10 +563,6 @@
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   is "ffold_raw"
 
-lemma funion_sym_pre:
-  "xs @ ys \<approx> ys @ xs"
-  by auto
-
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
   by auto
@@ -760,13 +756,9 @@
   shows "S |\<union>| {||} = S"
   by (lifting append_Nil2)
 
-lemma funion_sym:
-  shows "S |\<union>| T = T |\<union>| S"
-  by (lifting funion_sym_pre)
+thm sup.commute[where 'a="'a fset"]
 
-lemma funion_assoc:
-  shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
-  by (lifting append_assoc)
+thm sup.assoc[where 'a="'a fset"]
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
@@ -774,7 +766,7 @@
 
 lemma singleton_union_right:
   "S |\<union>| {|a|} = finsert a S"
-  by (subst funion_sym) simp
+  by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}