equal
deleted
inserted
replaced
125 (SpecParse.opt_thm_name ":" -- |
125 (SpecParse.opt_thm_name ":" -- |
126 OuterParse.term) -- |
126 OuterParse.term) -- |
127 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
127 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
128 OuterParse.term) |
128 OuterParse.term) |
129 |
129 |
130 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
130 val _ = OuterSyntax.local_theory "quotient_definition" |
131 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
131 "definition for constants over the quotient type" |
|
132 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
132 |
133 |
133 end; (* structure *) |
134 end; (* structure *) |
134 |
135 |
135 |
136 |
136 |
137 |