103 |
103 |
104 quotient_type myint = "nat \<times> nat" / intrel |
104 quotient_type myint = "nat \<times> nat" / intrel |
105 by (auto simp add: equivp_def expand_fun_eq) |
105 by (auto simp add: equivp_def expand_fun_eq) |
106 |
106 |
107 ML {* |
107 ML {* |
108 test_funs absF @{context} |
108 test_funs AbsF @{context} |
109 (@{typ "nat \<times> nat"}, |
109 (@{typ "nat \<times> nat"}, |
110 @{typ "myint"}) |
110 @{typ "myint"}) |
111 *} |
111 *} |
112 |
112 |
113 ML {* |
113 ML {* |
114 test_funs absF @{context} |
114 test_funs AbsF @{context} |
115 (@{typ "('a * 'a) list"}, |
115 (@{typ "('a * 'a) list"}, |
116 @{typ "'a foo"}) |
116 @{typ "'a foo"}) |
117 *} |
117 *} |
118 |
118 |
119 ML {* |
119 ML {* |
120 test_funs repF @{context} |
120 test_funs RepF @{context} |
121 (@{typ "(('a * 'a) list * 'b)"}, |
121 (@{typ "(('a * 'a) list * 'b)"}, |
122 @{typ "('a foo * 'b)"}) |
122 @{typ "('a foo * 'b)"}) |
123 *} |
123 *} |
124 |
124 |
125 ML {* |
125 ML {* |
126 test_funs absF @{context} |
126 test_funs AbsF @{context} |
127 (@{typ "(('a list) * int) list"}, |
127 (@{typ "(('a list) * int) list"}, |
128 @{typ "('a fset) bar"}) |
128 @{typ "('a fset) bar"}) |
129 *} |
129 *} |
130 |
130 |
131 ML {* |
131 ML {* |
132 test_funs absF @{context} |
132 test_funs AbsF @{context} |
133 (@{typ "('a list)"}, |
133 (@{typ "('a list)"}, |
134 @{typ "('a fset)"}) |
134 @{typ "('a fset)"}) |
135 *} |
135 *} |
136 |
136 |
137 ML {* |
137 ML {* |
138 test_funs absF @{context} |
138 test_funs AbsF @{context} |
139 (@{typ "('a list) list"}, |
139 (@{typ "('a list) list"}, |
140 @{typ "('a fset) fset"}) |
140 @{typ "('a fset) fset"}) |
141 *} |
141 *} |
142 |
142 |
143 |
143 |
144 ML {* |
144 ML {* |
145 test_funs absF @{context} |
145 test_funs AbsF @{context} |
146 (@{typ "((nat * nat) list) list"}, |
146 (@{typ "((nat * nat) list) list"}, |
147 @{typ "((myint) fset) fset"}) |
147 @{typ "((myint) fset) fset"}) |
148 *} |
148 *} |
149 |
149 |
150 ML {* |
150 ML {* |
151 test_funs absF @{context} |
151 test_funs AbsF @{context} |
152 (@{typ "(('a * 'a) list) list"}, |
152 (@{typ "(('a * 'a) list) list"}, |
153 @{typ "(('a * 'a) fset) fset"}) |
153 @{typ "(('a * 'a) fset) fset"}) |
154 *} |
154 *} |
155 |
155 |
156 ML {* |
156 ML {* |
157 test_funs absF @{context} |
157 test_funs AbsF @{context} |
158 (@{typ "(nat * nat) list"}, |
158 (@{typ "(nat * nat) list"}, |
159 @{typ "myint fset"}) |
159 @{typ "myint fset"}) |
160 *} |
160 *} |
161 |
161 |
162 ML {* |
162 ML {* |
163 test_funs absF @{context} |
163 test_funs AbsF @{context} |
164 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
164 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
165 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
165 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
166 *} |
166 *} |
167 |
167 |
168 lemma OO_sym_inv: |
168 lemma OO_sym_inv: |