--- a/Quot/Examples/AbsRepTest.thy Tue Jan 05 17:06:51 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy Tue Jan 05 17:12:35 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}
@@ -126,7 +131,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)"
using a1
apply -
sorry