--- a/FSet.thy	Wed Dec 02 14:11:46 2009 +0100
+++ b/FSet.thy	Wed Dec 02 14:37:21 2009 +0100
@@ -419,6 +419,33 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 done
 
+quotient fset2 = "'a list" / "list_eq"
+  apply(rule equiv_list_eq)
+  done
+
+quotient_def
+  EMPTY2 :: "'a fset2"
+where
+  "EMPTY2 \<equiv> ([]::'a list)"
+
+quotient_def
+  INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+where
+  "INSERT2 \<equiv> op #"
+
+ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *}
+ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty quot [rel_refl] [trans2] *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty quot defs *}
+
+lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
+lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+done
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where