equal
deleted
inserted
replaced
142 (* the auxiliary data for the quotient types *) |
142 (* the auxiliary data for the quotient types *) |
143 use "quotient_info.ML" |
143 use "quotient_info.ML" |
144 |
144 |
145 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
147 |
147 (* Throws now an exception: *) |
148 (* FIXME: This should throw an exception: *) |
|
149 (* declare [[map "option" = (bla, blu)]] *) |
148 (* declare [[map "option" = (bla, blu)]] *) |
150 |
149 |
151 |
150 |
152 (* identity quotient is not here as it has to be applied first *) |
151 (* identity quotient is not here as it has to be applied first *) |
153 lemmas [quotient_thm] = |
152 lemmas [quotient_thm] = |
158 |
157 |
159 (* fun_map is not here since equivp is not true *) |
158 (* fun_map is not here since equivp is not true *) |
160 (* TODO: option, ... *) |
159 (* TODO: option, ... *) |
161 lemmas [quotient_equiv] = |
160 lemmas [quotient_equiv] = |
162 identity_equivp prod_equivp |
161 identity_equivp prod_equivp |
163 |
|
164 ML {* maps_lookup @{theory} "*" *} |
|
165 ML {* maps_lookup @{theory} "fun" *} |
|
166 |
162 |
167 |
163 |
168 (* definition of the quotient types *) |
164 (* definition of the quotient types *) |
169 (* FIXME: should be called quotient_typ.ML *) |
165 (* FIXME: should be called quotient_typ.ML *) |
170 use "quotient.ML" |
166 use "quotient.ML" |