equal
deleted
inserted
replaced
89 |
89 |
90 fun quotient_lift_const qtys (b, t) ctxt = |
90 fun quotient_lift_const qtys (b, t) ctxt = |
91 quotient_def ((NONE, NoSyn), (Attrib.empty_binding, |
91 quotient_def ((NONE, NoSyn), (Attrib.empty_binding, |
92 (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt |
92 (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt |
93 |
93 |
94 local |
94 val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where" |
95 structure P = OuterParse; |
|
96 in |
|
97 |
|
98 val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where" |
|
99 |
95 |
100 val quotdef_parser = |
96 val quotdef_parser = |
101 Scan.optional quotdef_decl (NONE, NoSyn) -- |
97 Scan.optional quotdef_decl (NONE, NoSyn) -- |
102 P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term)) |
98 Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term)) |
103 end |
|
104 |
99 |
105 val _ = |
100 val _ = |
106 OuterSyntax.local_theory "quotient_definition" |
101 Outer_Syntax.local_theory "quotient_definition" |
107 "definition for constants over the quotient type" |
102 "definition for constants over the quotient type" |
108 OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |
103 Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |
109 |
104 |
110 end; (* structure *) |
105 end; (* structure *) |