diff -r 3b21b24a5fb6 -r a24e26f5488c Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Wed Dec 23 10:31:54 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Wed Dec 23 13:23:33 2009 +0100
@@ -2,31 +2,12 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
-
-(*
 quotient_type 
   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(auto)
-  sorry
   done
-*)
-
-inductive
-  list_eq (infix "\<approx>" 50)
-where
-  "a#b#xs \<approx> b#a#xs"
-| "[] \<approx> []"
-| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
-| "a#a#xs \<approx> a#xs"
-| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
-| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
-
-quotient_type 
-  fset = "'a list" / "list_eq"
-  sorry
-
 
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -36,7 +17,6 @@
 quotient_type int = "nat \<times> nat" / intrel
   sorry
 
-
 ML {*
 open Quotient_Term;
 *}