equal
deleted
inserted
replaced
56 |
56 |
57 (* defines the quotient types *) |
57 (* defines the quotient types *) |
58 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
58 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
59 let |
59 let |
60 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
60 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
61 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
61 val qty_args2 = (map2 (fn descr => fn args1 => (descr, args1, NONE)) qtys_descr qty_args1) |
62 in |
62 val qty_args3 = qty_args2 ~~ alpha_equivp_thms |
63 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
63 in |
|
64 fold_map Quotient_Type.add_quotient_type qty_args3 lthy |
64 end |
65 end |
65 |
66 |
66 |
67 |
67 (* defines quotient constants *) |
68 (* defines quotient constants *) |
68 fun define_qconsts qtys consts_specs lthy = |
69 fun define_qconsts qtys consts_specs lthy = |