# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262711420 -3600
# Node ID 77506496e6fd4cd691be3b24ea541994b2ac9337
# Parent  18b71981c1f0fbecdb42148a2e785af9b04abc4f# Parent  e038928daa678ce3ebad7a56038a034a6d3cba3b
merge

diff -r 18b71981c1f0 -r 77506496e6fd Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 05 18:09:03 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 05 18:10:20 2010 +0100
@@ -95,6 +95,11 @@
 *}
 
 
+ML {*
+test_funs absF @{context} 
+     (@{typ "((nat * nat) list) list"}, 
+      @{typ "((myint) fset) fset"})
+*}
 
 ML {*
 test_funs absF @{context} 
@@ -133,7 +138,8 @@
 lemma bla:
   assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
   and     a2:  "Quotient r2 abs2 rep2"
-  shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
+  shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) 
+               (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
 apply (rule)+
 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset])