diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Thu Dec 24 00:58:50 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Dec 24 22:28:19 2009 +0100
@@ -5,7 +5,14 @@
 print_maps
 
 quotient_type 
-  fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  done
+
+quotient_type 
+  'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * '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)
@@ -17,13 +24,11 @@
 Quotient_Info.quotient_rules_get @{context}
 *}
 
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
-  sorry
+quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)"
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  done
 
 print_quotients
 
@@ -32,11 +37,23 @@
 *}
 
 ML {*
-absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"})
+absrep_fun_chk absF @{context} 
+     (@{typ "(('a * 'a) list) list"}, 
+      @{typ "(('a * 'a) fset) fset"})
 |> Syntax.string_of_term @{context}
 |> writeln
 *}
 
+(*
+ML {*
+absrep_fun_chk absF @{context} 
+     (@{typ "('a * 'a) list"}, 
+      @{typ "'a foo"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+*)
+
 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"
 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"
 term "option_map (map rep_int \<circ> rep_fset)"