# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256663145 -3600
# Node ID 80859cc80332dd99144f175b91b3e241d374e887
# Parent  f88ea69331bfb6a9a6d83a950faa5be520ee2e30
Manual conversion of equality to equivalence allows lifting append_assoc.

diff -r f88ea69331bf -r 80859cc80332 FSet.thy
--- a/FSet.thy	Tue Oct 27 18:02:35 2009 +0100
+++ b/FSet.thy	Tue Oct 27 18:05:45 2009 +0100
@@ -468,6 +468,9 @@
 *}
 ML fset_defs
 
+lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
+by (simp add: list_eq_refl)
+
 
 ML {* lift @{thm m2} *}
 ML {* lift @{thm m1} *}
@@ -475,7 +478,7 @@
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
 ML {* lift @{thm map_append} *}
-(* ML {* lift @{thm append_assoc} *}*)
+ML {* lift @{thm eq_r[OF append_assoc]} *}
 
 thm