equal
deleted
inserted
replaced
216 (* - its free type variables (first argument) *) |
216 (* - its free type variables (first argument) *) |
217 (* - its mixfix annotation *) |
217 (* - its mixfix annotation *) |
218 (* - the type to be quotient *) |
218 (* - the type to be quotient *) |
219 (* - the relation according to which the type is quotient *) |
219 (* - the relation according to which the type is quotient *) |
220 (* *) |
220 (* *) |
221 (* opens a proof-state in which one has to show that the *) |
221 (* it opens a proof-state in which one has to show that the *) |
222 (* relation is an equivalence relation *) |
222 (* relations are equivalence relations *) |
223 |
223 |
224 fun quotient_type quot_list lthy = |
224 fun quotient_type quot_list lthy = |
225 let |
225 let |
226 (* sanity check *) |
226 (* sanity check *) |
227 val _ = map sanity_check quot_list |
227 val _ = map sanity_check quot_list |