equal
deleted
inserted
replaced
10 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |
10 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |
11 local_theory -> (term * thm) * local_theory |
11 local_theory -> (term * thm) * local_theory |
12 |
12 |
13 val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> |
13 val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> |
14 local_theory -> (term * thm) * local_theory |
14 local_theory -> (term * thm) * local_theory |
|
15 |
|
16 val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory |
15 end; |
17 end; |
16 |
18 |
17 structure Quotient_Def: QUOTIENT_DEF = |
19 structure Quotient_Def: QUOTIENT_DEF = |
18 struct |
20 struct |
19 |
21 |
83 val lthy'' = Variable.declare_term rhs lthy' |
85 val lthy'' = Variable.declare_term rhs lthy' |
84 in |
86 in |
85 quotient_def (decl, (attr, (lhs, rhs))) lthy'' |
87 quotient_def (decl, (attr, (lhs, rhs))) lthy'' |
86 end |
88 end |
87 |
89 |
|
90 fun quotient_lift_const (b, t) ctxt = |
|
91 quotient_def ((NONE, NoSyn), (Attrib.empty_binding, |
|
92 (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt |
|
93 |
88 local |
94 local |
89 structure P = OuterParse; |
95 structure P = OuterParse; |
90 in |
96 in |
91 |
97 |
92 val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where" |
98 val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where" |