equal
deleted
inserted
replaced
1 |
1 |
2 signature QUOTIENT_DEF = |
2 signature QUOTIENT_DEF = |
3 sig |
3 sig |
4 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
4 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
5 Proof.context -> (term * thm) * local_theory |
5 local_theory -> (term * thm) * local_theory |
6 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
6 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
7 local_theory -> local_theory |
7 local_theory -> local_theory |
8 end; |
8 end; |
9 |
9 |
10 structure Quotient_Def: QUOTIENT_DEF = |
10 structure Quotient_Def: QUOTIENT_DEF = |