equal
deleted
inserted
replaced
93 (@{typ "('a list) list"}, |
93 (@{typ "('a list) list"}, |
94 @{typ "('a fset) fset"}) |
94 @{typ "('a fset) fset"}) |
95 *} |
95 *} |
96 |
96 |
97 |
97 |
|
98 ML {* |
|
99 test_funs absF @{context} |
|
100 (@{typ "((nat * nat) list) list"}, |
|
101 @{typ "((myint) fset) fset"}) |
|
102 *} |
98 |
103 |
99 ML {* |
104 ML {* |
100 test_funs absF @{context} |
105 test_funs absF @{context} |
101 (@{typ "(('a * 'a) list) list"}, |
106 (@{typ "(('a * 'a) list) list"}, |
102 @{typ "(('a * 'a) fset) fset"}) |
107 @{typ "(('a * 'a) fset) fset"}) |
124 done |
129 done |
125 |
130 |
126 lemma bla: |
131 lemma bla: |
127 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
132 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
128 and a2: "Quotient r2 abs2 rep2" |
133 and a2: "Quotient r2 abs2 rep2" |
129 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
134 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
|
135 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
130 using a1 |
136 using a1 |
131 apply - |
137 apply - |
132 sorry |
138 sorry |
133 |
139 |
134 lemma bla2: |
140 lemma bla2: |